mpri-funcprog-project/coq
2017-10-05 17:57:33 +02:00
..
.gitignore Coq demo. 2017-09-21 15:40:42 +02:00
Autosubst_Env.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
Autosubst_EOS.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
Autosubst_FreeVars.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
Autosubst_IsRen.v Expose more Coq files. 2017-09-28 10:36:07 +02:00
AutosubstExtra.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
ClosureConversion.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
DemoSyntaxReduction.v Updated slides, Coq demo, and OCaml exercise. 2017-09-22 11:32:50 +02:00
Even.v Added Even.v. 2017-09-26 16:50:45 +02:00
LambdaCalculusBigStep.v Remove marks in Coq files. 2017-09-28 15:15:51 +02:00
LambdaCalculusFreeVars.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
LambdaCalculusInterpreter.v Remove marks in Coq files. 2017-09-28 15:15:51 +02:00
LambdaCalculusReduction.v Expose more Coq files. 2017-09-28 10:36:07 +02:00
LambdaCalculusSyntax.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
LambdaCalculusValues.v Expose more Coq files. 2017-09-28 10:36:07 +02:00
Makefile Coq demo. 2017-09-21 15:40:42 +02:00
Makefile.coq Coq demo. 2017-09-21 15:40:42 +02:00
MetaBigStep.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
MetalBigStep.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
MetalSyntax.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
MyList.v Expose new Coq files. 2017-10-05 17:57:33 +02:00
MyTactics.v Coq demo. 2017-09-21 15:40:42 +02:00
Option.v Expose more Coq files. 2017-09-28 10:36:07 +02:00
README.md Add coq/README.md. 2017-09-28 10:36:55 +02:00
Sequences.v Expose more Coq files. 2017-09-28 10:36:07 +02:00

This code has been tested with Coq 8.5pl3.

For now, this code requires my slightly patched version of Autosubst. To install this library, proceed as follows:

  git clone git@github.com:fpottier/autosubst.git
  cd autosubst
  make && make install

You can then compile the Coq code as follows:

  make _CoqProject
  make -j4