Proving converse of the equivalence of contextual refinement definitions #19

	name: CI

	on:
	push:
	branches:
	- main
	pull_request:
	branches:
	- '**'

	jobs:
	build:
	runs-on: ubuntu-latest
	strategy:
	matrix:
	coq_version:
	- '8.16.1'
	ocaml_version:
	- '4.14.1-flambda'
	max-parallel: 4
	# don't cancel all in-progress jobs if one matrix job fails:
	fail-fast: false

	steps:
	- uses: actions/checkout@v3
	- uses: coq-community/docker-coq-action@v1
	with:
	opam_file: 'clutch.opam'
	coq_version: ${{ matrix.coq_version }}
	ocaml_version: ${{ matrix.ocaml_version }}
	before_script: \|
	sudo chown -R coq:coq . # workaround a permission issue
	script: \|
	startGroup Build
	make -j2
	endGroup
	uninstall: \|
	make clean
	- name: Revert permissions
	# to avoid a warning at cleanup time
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

Provide feedback