remove contra-variant subtyping #58

	name: CI build
	on:
	push:
	branches:
	- main
	pull_request:
	branches:
	- main

	env:
	REGISTRY: "ghcr.io"
	IMAGE_TAG: "beluga-lang/mcltt:main"

	jobs:
	wf:
	name: Completeness of _CoqProject
	runs-on: ubuntu-latest
	steps:
	- name: repo checkout
	uses: actions/checkout@v3
	- name: check
	run: \|
	.github/scripts/check_projects.sh theories

	build:
	name: Continuous Intergration
	runs-on: ubuntu-latest
	permissions:
	packages: read
	steps:
	- name: get number of CPU cores
	uses: SimenB/github-actions-cpu-cores@v2
	id: cpu-cores

	- name: repo checkout
	uses: actions/checkout@v3

	- name: container registry log in
	uses: docker/login-action@v3
	with:
	registry: ${{ env.REGISTRY }}
	username: ${{ github.actor }}
	password: ${{ secrets.GITHUB_TOKEN }}

	- name: image pre-pulling
	run: docker pull ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }}

	- name: coq processing
	uses: coq-community/docker-coq-action@v1
	with:
	custom_image: ${{ env.REGISTRY }}/${{ env.IMAGE_TAG }}
	install: \|
	before_script: \|
	startGroup "Fix the permission issue"
	sudo chown -R coq:coq .
	endGroup
	script: \|
	startGroup "Build Coq lib"
	cd theories/
	make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
	endGroup
	after_script: \|
	startGroup "Test parser"
	dune build
	dune runtest
	endGroup
	export: "OPAMJOBS OPAMYES"
	env:
	OPAMJOBS: ${{ steps.cpu-cores.outputs.count }}
	OPAMYES: "true"

	- name: permissions revert
	# to avoid a warning at cleanup time
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

Provide feedback