coq export: use Require Export instead of Require Import #2362

	on:
	pull_request:
	types: [opened, synchronize, edited, reopened]
	push:
	workflow_dispatch:
	jobs:
	build_lambdapi:
	strategy:
	fail-fast: false
	matrix:
	ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
	runs-on: ubuntu-latest
	steps:
	- name: checking out lambdapi repo ...
	uses: actions/checkout@v4
	- name: recovering cached opam files ...
	uses: actions/cache@v4
	with:
	path: ~/.opam
	key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
	- name: setting up opam ...
	uses: avsm/setup-ocaml@v3
	with:
	ocaml-compiler: ${{ matrix.ocaml-version }}
	- name: installing dependencies ...
	run: \|
	opam update
	opam upgrade
	opam pin add -n -k path lambdapi .
	opam install --deps-only -d -t lambdapi
	- name: running tests ...
	run: \|
	make sanity_check
	eval $(opam env)
	#why3 config detect
	make tests
	build_vscode_extension:
	strategy:
	fail-fast: false
	runs-on: ubuntu-latest
	steps:
	- name: checking out lambdapi repo ...
	uses: actions/checkout@v4
	- name: Use Node.js
	uses: actions/setup-node@v4
	with:
	node-version: latest
	- name: generate-vscode-extension
	run: \|
	npm install -g @types/vscode
	npm install -g @vscode/vsce
	make build-vscode-extension
	make publish-vscode-extension
	env:
	PAT: ${{ secrets.VSCODE_PAT }}
	- name: upload vscode extension
	uses: actions/upload-artifact@v4
	with:
	name: assets-for-download
	path: editors/vscode/extensionFolder

Provide feedback