Skip to content

Commit

Permalink
Update
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Dec 14, 2023
1 parent aae3008 commit 5060e67
Show file tree
Hide file tree
Showing 4 changed files with 1,931 additions and 2 deletions.
3 changes: 1 addition & 2 deletions proof-libs/coq/coq/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ opam install coq-compcert coq-coqprime

## Compiling the coq files

In folder `/coq`, type `make`. This compiles the coq libraries and the compiled examples, as defined in `_CoqProject`.
This requires the coq compiler to be installed (only tested on coq 8.13.1)
In folder `/coq`, type `make`. This compiles the coq libraries and the compiled examples, as defined in `_CoqProject`. This requires the coq compiler to be installed.

If you want to add a new example to `_CoqProject`, such that it is compiled through `make`, you should run `coq_makefile -f _CoqProject -o Makefile` in `/coq` to update the makefile.
1 change: 1 addition & 0 deletions proof-libs/coq/coq/_CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,5 @@

src/MachineIntegers.v
src/Hacspec_Lib.v
src/Hacspec_lib.v
src/QuickChickLib.v

0 comments on commit 5060e67

Please sign in to comment.