Commit cc4aaa06 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix Coq backend for new validator, check version in Coq parsers.

parent 98a73d83
......@@ -160,6 +160,8 @@ release:
@ git add src/StaticVersion.ml src/StaticVersion.mli
@ echo '\gdef\menhirversion{$(DATE)}' > doc/version.tex
@ git add doc/version.tex
@ echo 'Definition require_$(DATE).' >> coq-menhirlib/src/Version.v
@ git add coq-menhirlib/src/Version.v
# Compile the documentation.
@ echo "Building the documentation..."
@ make --quiet -C doc clean >/dev/null
......
......@@ -7,12 +7,15 @@ export
.PHONY: all clean install uninstall
all:
_CoqProject:
@ $(MAKE) -f Makefile.coq --no-print-directory _CoqProject
all: _CoqProject
@ $(MAKE) -f Makefile.coq --no-print-directory all
clean:
@ $(MAKE) -f Makefile.coq --no-print-directory clean
@ rm -f _CoqProject
CONTRIB := $(shell $(COQBIN)coqc -where)/user-contrib
TARGET := $(CONTRIB)/MenhirLib
......
Definition require_unreleased := tt.
This diff is collapsed.
......@@ -287,9 +287,6 @@ let set_echo_errors filename =
let cmly =
ref false
let coq_lib_path =
ref (Some "MenhirLib")
type dollars =
| DollarsDisallowed
| DollarsAllowed
......@@ -308,8 +305,6 @@ let options = Arg.align [
"--compare-errors", Arg.String add_compare_errors, "<filename> (used twice) Compare two .messages files";
"--compile-errors", Arg.String set_compile_errors, "<filename> Compile a .messages file to OCaml code";
"--coq", Arg.Set coq, " Generate a formally verified parser, in Coq";
"--coq-lib-path", Arg.String (fun path -> coq_lib_path := Some path), "<path> How to qualify references to MenhirLib";
"--coq-lib-no-path", Arg.Unit (fun () -> coq_lib_path := None), " Do *not* qualify references to MenhirLib";
"--coq-no-actions", Arg.Set coq_no_actions, " Ignore semantic actions in the Coq output";
"--coq-no-complete", Arg.Set coq_no_complete, " Do not generate a proof of completeness";
"--depend", Arg.Unit enable_depend, " Invoke ocamldep and display dependencies";
......@@ -595,9 +590,6 @@ let echo_errors =
let cmly =
!cmly
let coq_lib_path =
!coq_lib_path
let dollars =
!dollars
......
......@@ -232,12 +232,6 @@ val echo_errors: string option
val cmly: bool
(* This name is used in --coq mode. It appears in the generated Coq file,
and indicates under what name (or path) the Coq library MenhirLib is
known. Its default value is [Some "MenhirLib"]. *)
val coq_lib_path: string option
(* This flag tells whether [$i] notation in semantic actions is allowed. *)
type dollars =
......
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