Commit cec5e7ec authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Misc adjustments regarding coq-minicalc.

parent d46683e3
Pipeline #95552 passed with stages
in 27 seconds
......@@ -8,6 +8,9 @@
# The following demos require menhirSdk and OCaml >= 4.03:
# generate-printers
# The following demos require coq-menhirlib:
# coq-minicalc
# The demos whose name ends in -dune require dune 1.4.
# If dune is absent, attempting to build these demos
# succeeds without actually doing anything.
......
Parser.v
.*.aux
.*.d
Makefile.coq
Makefile.coq.conf
*.glob
......@@ -6,10 +6,10 @@ Pierre Letouzey, 2019
Licence : CC0
This is a toy demo of the recent Coq backend of `menhir`.
This is a toy demo of the Coq backend of `menhir`.
This micro-grammar recognizes arithmetic expressions : numbers, idents, `+` `*` `-` `/` and parenthesis.
We provide an hand-written lexer, and a minimal final test (compilation should display "OK").
This micro-grammar recognizes arithmetic expressions : numbers, idents, `+` `*` `-` `/` and parentheses.
We provide a hand-written lexer and a minimal final test (compilation should display "OK").
Tested with Coq 8.8 + menhir 2019/06/13 + corresponding coq-menhirlib.
Anything more recent than that should be ok.
\ No newline at end of file
Anything more recent than that should be ok.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment