Commit 70ddd069 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make optional the version check for the Coq backend

parent decd6ec9
......@@ -514,10 +514,12 @@ module Run (T: sig end) = struct
fprintf f "From Coq.Lists Require List.\n";
fprintf f "From Coq.Numbers Require Import BinNums.\n";
from_menhirlib f; fprintf f "Require Main.\n";
from_menhirlib f; fprintf f "Require Version.\n";
if not Settings.coq_no_version_check then
from_menhirlib f; fprintf f "Require Version.\n";
fprintf f "Import List.ListNotations.\n\n";
fprintf f "Definition version_check : unit := %sVersion.require_%s.\n\n" menhirlib_path Version.version;
if not Settings.coq_no_version_check then
fprintf f "Definition version_check : unit := %sVersion.require_%s.\n\n" menhirlib_path Version.version;
fprintf f "Unset Elimination Schemes.\n\n";
......
......@@ -223,6 +223,9 @@ let inspection =
let coq =
ref false
let coq_no_version_check =
ref false
let coq_no_complete =
ref false
......@@ -310,6 +313,7 @@ let options = Arg.align [
"--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-version-check", Arg.Set coq_no_version_check, " The generated parser will not check that the versions of Menhir and MenhirLib match.";
"--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";
......@@ -547,6 +551,9 @@ let () =
let coq =
!coq
let coq_no_version_check =
!coq_no_version_check
let coq_no_complete =
!coq_no_complete
......
......@@ -163,6 +163,10 @@ val inspection : bool
val coq : bool
(* Whether to generate a version check for MenhirLib in the generated parser. *)
val coq_no_version_check : bool
(* Whether the coq description must contain completeness proofs. *)
val coq_no_complete : bool
......
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