Fix the proof using a hole in the guard checker #33

	name: MetaRocq CI

	on:
	push:
	pull_request:
	types: [opened, synchronize, reopened, ready_for_review]

	jobs:
	checktodos:
	if: github.event_name != 'pull_request' \|\| github.event.pull_request.draft == false
	runs-on: ubuntu-latest
	steps:
	- name: Checkout code
	uses: actions/checkout@v4
	with:
	fetch-depth: 1

	- name: Check for todos
	run: ./checktodos.sh

	build:
	runs-on: ubuntu-latest

	strategy:
	matrix:
	coq_version:
	- '9.0'
	ocaml_version:
	- '4.14-flambda'
	# - '4.09-flambda'
	target: [ local, opam ]
	fail-fast: true

	concurrency:
	group: ${{ github.workflow }}-${{ matrix.ocaml_version }}-${{ matrix.target }}-Ubuntu-${{ github.event_name }}-${{ github.head_ref \|\| github.run_id }}
	cancel-in-progress: true

	steps:

	- name: Checkout code
	uses: actions/checkout@v4
	with:
	fetch-depth: 1

	- name: Docker-Coq-Action
	uses: coq-community/docker-coq-action@v1
	with:
	coq_version: ${{ matrix.coq_version }}
	ocaml_version: ${{ matrix.ocaml_version }}
	before_install: \|
	startGroup "Print opam config"
	opam config list; opam repo list; opam list
	endGroup
	startGroup "Workaround permission issue"
	sudo chown -R 1000:1000 .
	endGroup
	script: \|
	startGroup "Build project"
	opam exec -- ./configure.sh --enable-${{matrix.target}}
	opam exec -- make -j 2 ci-${{matrix.target}}
	endGroup
	# Already done by the ci-opam target
	uninstall: \|
	startGroup "Clean project"
	endGroup
	- name: Revert permissions
	# to avoid a warning at cleanup time
	if: ${{ always() }}
	run: sudo chown -R 1001:116 . # <--

Provide feedback