aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
commitb75f714c025b51ed8b4db15bfce99df2d6ae7c41 (patch)
tree4c25d6cbc0d6f62450c15ebdda03a3ada717c8e1
parentb1714dcc7df330df92a935f202964a1e73e44652 (diff)
parent7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb (diff)
Merge PR #7558: [api] Make `vernac/` self-contained.
-rw-r--r--META.coq24
-rw-r--r--dev/base_include2
-rw-r--r--dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh14
-rw-r--r--dev/doc/changes.md12
-rw-r--r--parsing/parsing.mllib5
-rw-r--r--parsing/pcoq.ml41
-rw-r--r--parsing/pcoq.mli34
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/g_ltac.ml48
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/g_tactic.ml42
-rw-r--r--plugins/ssr/ssrvernac.ml42
-rw-r--r--printing/printing.mllib1
-rw-r--r--stm/stm.ml2
-rw-r--r--tactics/hints.ml21
-rw-r--r--tactics/hints.mli21
-rw-r--r--toplevel/g_toplevel.ml42
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/egramcoq.ml (renamed from parsing/egramcoq.ml)0
-rw-r--r--vernac/egramcoq.mli (renamed from parsing/egramcoq.mli)0
-rw-r--r--vernac/egramml.ml (renamed from parsing/egramml.ml)2
-rw-r--r--vernac/egramml.mli (renamed from parsing/egramml.mli)0
-rw-r--r--vernac/g_proofs.ml4 (renamed from parsing/g_proofs.ml4)2
-rw-r--r--vernac/g_vernac.ml4 (renamed from parsing/g_vernac.ml4)2
-rw-r--r--vernac/metasyntax.ml10
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/ppvernac.ml (renamed from printing/ppvernac.ml)2
-rw-r--r--vernac/ppvernac.mli (renamed from printing/ppvernac.mli)0
-rw-r--r--vernac/pvernac.ml56
-rw-r--r--vernac/pvernac.mli36
-rw-r--r--vernac/vernac.mllib15
-rw-r--r--vernac/vernacentries.ml4
-rw-r--r--vernac/vernacexpr.ml (renamed from parsing/vernacexpr.ml)17
35 files changed, 225 insertions, 126 deletions
diff --git a/META.coq b/META.coq
index 8d4c3d5f0..cdc088e74 100644
--- a/META.coq
+++ b/META.coq
@@ -6,6 +6,18 @@ version = "8.8"
directory = ""
requires = "camlp5"
+package "grammar" (
+
+ description = "Coq Camlp5 Grammar Extensions for Plugins"
+ version = "8.8"
+
+ requires = "camlp5.gramlib"
+ directory = "grammar"
+
+ archive(byte) = "grammar.cma"
+ archive(native) = "grammar.cmxa"
+)
+
package "config" (
description = "Coq Configuration Variables"
@@ -126,18 +138,6 @@ package "interp" (
)
-package "grammar" (
-
- description = "Coq Camlp5 Grammar Extensions for Plugins"
- version = "8.8"
-
- requires = "camlp5.gramlib"
- directory = "grammar"
-
- archive(byte) = "grammar.cma"
- archive(native) = "grammar.cmxa"
-)
-
package "proofs" (
description = "Coq Proof Engine"
diff --git a/dev/base_include b/dev/base_include
index 8d81ca3e0..fc38305cc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -189,7 +189,7 @@ let qid = Libnames.qualid_of_string;;
(* parsing of terms *)
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;;
let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
(* build a term of type glob_constr without type-checking or resolution of
diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
new file mode 100644
index 000000000..115f29f1e
--- /dev/null
+++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then
+
+ _OVERLAY_BRANCH=vernac+move_parser
+
+ Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index cd28b1b50..346b7c7dd 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,7 +4,7 @@
Misctypes
- Syntax for universe sorts and kinds has been moved from `Misctypes`
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
to `Glob_term`, as these are turned into kernel terms by
`Pretyping`.
@@ -41,6 +41,16 @@ Printer.ml API
pr_subgoal and pr_goal was removed to simplify the code. It was
earlierly used by PCoq.
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+ is self-contained now, including the parsing and extension
+ mechanisms. This involves a couple of non-backward compatible
+ changes due to layering issues, where some functions have been moved
+ from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+ `tactics/`. In all cases adapting is a matter of changing the module
+ name.
+
### Unit testing
The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 103e1188a..da4a0421b 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,11 +1,6 @@
Tok
CLexer
Extend
-Vernacexpr
Pcoq
-Egramml
-Egramcoq
G_constr
-G_vernac
G_prim
-G_proofs
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 258c4bb11..b78c35c26 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -145,7 +145,6 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
end
-
let warning_verbose = Gramext.warning_verbose
let of_coq_assoc = function
@@ -387,7 +386,6 @@ let create_universe u =
let uprim = create_universe "prim"
let uconstr = create_universe "constr"
let utactic = create_universe "tactic"
-let uvernac = create_universe "vernac"
let get_univ u =
if Hashtbl.mem utables u then u
@@ -493,44 +491,6 @@ module Module =
let module_type = Gram.entry_create "module_type"
end
-module Vernac_ =
- struct
- let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
-
- (* The different kinds of vernacular commands *)
- let gallina = gec_vernac "gallina"
- let gallina_ext = gec_vernac "gallina_ext"
- let command = gec_vernac "command"
- let syntax = gec_vernac "syntax_command"
- let vernac_control = gec_vernac "Vernac.vernac_control"
- let rec_definition = gec_vernac "Vernac.rec_definition"
- let red_expr = make_gen_entry utactic "red_expr"
- let hint_info = gec_vernac "hint_info"
- (* Main vernac entry *)
- let main_entry = Gram.entry_create "vernac"
- let noedit_mode = gec_vernac "noedit_command"
-
- let () =
- let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
- let act_eoi = Gram.action (fun _ loc -> None) in
- let rule = [
- ([ Symbols.stoken Tok.EOI ], act_eoi);
- ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
- ] in
- uncurry (Gram.extend main_entry) (None, make_rule rule)
-
- let command_entry_ref = ref noedit_mode
- let command_entry =
- Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
-
- end
-
-let main_entry = Vernac_.main_entry
-
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
-
let epsilon_value f e =
let r = Rule (Next (Stop, e), fun x _ -> f x) in
let ext = of_coq_extend_statement (None, [None, None, [r]]) in
@@ -635,7 +595,6 @@ let () =
Grammar.register0 wit_ref (Prim.reference);
Grammar.register0 wit_sort_family (Constr.sort_family);
Grammar.register0 wit_constr (Constr.constr);
- Grammar.register0 wit_red_expr (Vernac_.red_expr);
()
(** Registering extra grammar *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 387a62604..36e5e420a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -10,12 +10,10 @@
open Names
open Extend
-open Vernacexpr
open Genarg
open Constrexpr
open Libnames
open Misctypes
-open Genredexpr
(** The parser of Coq *)
@@ -89,6 +87,12 @@ module type S =
end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
+module Symbols : sig
+
+ val stoken : Tok.t -> Gram.symbol
+ val snterm : Gram.internal_entry -> Gram.symbol
+end
+
(** The parser of Coq is built from three kinds of rule declarations:
- dynamic rules declared at the evaluation of Coq files (using
@@ -177,11 +181,14 @@ val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
type gram_universe
val get_univ : string -> gram_universe
+val create_universe : string -> gram_universe
+
+val new_entry : gram_universe -> string -> 'a Gram.entry
val uprim : gram_universe
val uconstr : gram_universe
val utactic : gram_universe
-val uvernac : gram_universe
+
val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
@@ -249,27 +256,6 @@ module Module :
val module_type : module_ast Gram.entry
end
-module Vernac_ :
- sig
- val gallina : vernac_expr Gram.entry
- val gallina_ext : vernac_expr Gram.entry
- val command : vernac_expr Gram.entry
- val syntax : vernac_expr Gram.entry
- val vernac_control : vernac_control Gram.entry
- val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
- val noedit_mode : vernac_expr Gram.entry
- val command_entry : vernac_expr Gram.entry
- val red_expr : raw_red_expr Gram.entry
- val hint_info : Typeclasses.hint_info_expr Gram.entry
- end
-
-(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
-
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
-
val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** {5 Extending the parser without synchronization} *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d193e1144..0a2741ad1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -125,7 +125,7 @@ ARGUMENT EXTEND auto_using'
END
module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
+module Vernac = Pvernac.Vernac_
module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index c21921513..17011f206 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r =
let add_hints_iff ~atts l2r lc n bl =
let open Vernacinterp in
- Hints.add_hints (Locality.make_module_locality atts.locality) bl
+ Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
(Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99f..07047d016 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
fun ~atts ~st -> begin
let open Vernacinterp in
let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- Hints.add_hints (Locality.make_section_locality atts.locality)
+ Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
(match dbnames with None -> ["core"] | Some l -> l) entry;
st
end
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 4857beffa..ed54320a5 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -21,9 +21,9 @@ open Tok (* necessary for camlp5 *)
open Names
open Pcoq
-open Pcoq.Constr
-open Pcoq.Vernac_
open Pcoq.Prim
+open Pcoq.Constr
+open Pvernac.Vernac_
open Pltac
let fail_default_value = ArgArg 0
@@ -58,8 +58,8 @@ let tacdef_body = new_entry "tactic:tacdef_body"
let _ =
let mode = {
Proof_global.name = "Classic";
- set = (fun () -> set_command_entry tactic_mode);
- reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+ set = (fun () -> Pvernac.set_command_entry tactic_mode);
+ reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
} in
Proof_global.register_proof_mode mode
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fbaa2e58f..079001ee4 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -20,9 +20,9 @@ open Extraargs
open Tacmach
open Rewrite
open Stdarg
-open Pcoq.Vernac_
open Pcoq.Prim
open Pcoq.Constr
+open Pvernac.Vernac_
open Pltac
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 7534e2799..dc9f607cf 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -211,7 +211,7 @@ let warn_deprecated_eqn_syntax =
(* Auxiliary grammar rules *)
-open Vernac_
+open Pvernac.Vernac_
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7ac9ea89d..750461a1b 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -19,7 +19,7 @@ open Constrexpr_ops
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
open Ltac_plugin
open Notation_ops
open Notation_term
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 86b68d8fb..b69d8a9ef 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -4,4 +4,3 @@ Ppconstr
Printer
Printmod
Prettyp
-Ppvernac
diff --git a/stm/stm.ml b/stm/stm.ml
index b8fe8ddd7..c394be22e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2976,7 +2976,7 @@ let parse_sentence ~doc sid pa =
str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
Flags.with_option Flags.we_are_parsing (fun () ->
try
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+ match Pcoq.Gram.entry_parse Pvernac.main_entry pa with
| None -> raise End_of_input
| Some (loc, cmd) -> CAst.make ~loc cmd
with e when CErrors.noncritical e ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 786760122..7b5be4c1c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,7 +28,6 @@ open Termops
open Inductiveops
open Typing
open Decl_kinds
-open Vernacexpr
open Typeclasses
open Pattern
open Patternops
@@ -156,6 +155,24 @@ type full_hint = hint with_metadata
type hint_entry = GlobRef.t option *
raw_hint hint_ast with_uid with_metadata
+type reference_or_constr =
+ | HintsReference of reference
+ | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+ | ModeInput (* No evars *)
+ | ModeNoHeadEvar (* No evar at the head *)
+ | ModeOutput (* Anything *)
+
+type hints_expr =
+ | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of reference list
+ | HintsTransparency of reference list * bool
+ | HintsMode of reference * hint_mode list
+ | HintsConstructors of reference list
+ | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
type import_level = [ `LAX | `WARN | `STRICT ]
let warn_hint : import_level ref = ref `LAX
@@ -1326,7 +1343,7 @@ let interp_hints poly =
let _, tacexp = Genintern.generic_intern env tacexp in
HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c7de10a2a..f05988703 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -18,7 +18,6 @@ open Misctypes
open Tactypes
open Clenv
open Pattern
-open Vernacexpr
(** {6 General functions. } *)
@@ -71,6 +70,24 @@ type search_entry
type hint_entry
+type reference_or_constr =
+ | HintsReference of Libnames.reference
+ | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+ | ModeInput (* No evars *)
+ | ModeNoHeadEvar (* No evar at the head *)
+ | ModeOutput (* Anything *)
+
+type hints_expr =
+ | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of Libnames.reference list
+ | HintsTransparency of Libnames.reference list * bool
+ | HintsMode of Libnames.reference * hint_mode list
+ | HintsConstructors of Libnames.reference list
+ | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
| PathStar of 'a hints_path_gen
@@ -178,7 +195,7 @@ val current_pure_db : unit -> hint_db list
val interp_hints : polymorphic -> hints_expr -> hints_entry
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool (* Check no remaining evars *) ->
(bool * bool) (* polymorphic or monomorphic, local or global *) ->
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
index d5d558b9b..e3cefe236 100644
--- a/toplevel/g_toplevel.ml4
+++ b/toplevel/g_toplevel.ml4
@@ -35,7 +35,7 @@ GEXTEND Gram
| IDENT "Quit"; "." -> CAst.make VernacQuit
| IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
CAst.make (VernacBacktrack (n,m,p))
- | cmd = main_entry ->
+ | cmd = Pvernac.main_entry ->
match cmd with
| None -> raise Stm.End_of_input
| Some (loc,c) -> CAst.make ~loc (VernacControl c)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d99d45313..40001c0a3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option {
let typeclasses_db = "typeclass_instances"
let set_typeclass_transparency c local b =
- Hints.add_hints local [typeclasses_db]
+ Hints.add_hints ~local [typeclasses_db]
(Hints.HintsTransparencyEntry ([c], b))
let _ =
@@ -56,7 +56,7 @@ let _ =
(Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
info.hint_pattern } in
Flags.silently (fun () ->
- Hints.add_hints local [typeclasses_db]
+ Hints.add_hints ~local [typeclasses_db]
(Hints.HintsResolveEntry
[info, poly, false, Hints.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
diff --git a/parsing/egramcoq.ml b/vernac/egramcoq.ml
index 5f63d21c4..5f63d21c4 100644
--- a/parsing/egramcoq.ml
+++ b/vernac/egramcoq.ml
diff --git a/parsing/egramcoq.mli b/vernac/egramcoq.mli
index e15add10f..e15add10f 100644
--- a/parsing/egramcoq.mli
+++ b/vernac/egramcoq.mli
diff --git a/parsing/egramml.ml b/vernac/egramml.ml
index 90cd7d10b..048d4d93a 100644
--- a/parsing/egramml.ml
+++ b/vernac/egramml.ml
@@ -77,7 +77,7 @@ let get_extend_vernac_rule (s, i) =
| Failure _ -> raise Not_found
let extend_vernac_command_grammar s nt gl =
- let nt = Option.default Vernac_.command nt in
+ let nt = Option.default Pvernac.Vernac_.command nt in
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s, l) in
let rules = [make_rule mkact gl] in
diff --git a/parsing/egramml.mli b/vernac/egramml.mli
index 31aa1a989..31aa1a989 100644
--- a/parsing/egramml.mli
+++ b/vernac/egramml.mli
diff --git a/parsing/g_proofs.ml4 b/vernac/g_proofs.ml4
index 4f3d83a8a..56229c765 100644
--- a/parsing/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -16,7 +16,7 @@ open Misctypes
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
let thm_token = G_vernac.thm_token
diff --git a/parsing/g_vernac.ml4 b/vernac/g_vernac.ml4
index a1c563f53..6c7df8cfa 100644
--- a/parsing/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -25,8 +25,8 @@ open Tok (* necessary for camlp5 *)
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
open Pcoq.Module
+open Pvernac.Vernac_
let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
let _ = List.iter CLexer.add_keyword vernac_kw
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 76958b05f..e038f54dd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -76,15 +76,15 @@ let pr_grammar = function
pr_entry Pcoq.Constr.pattern
| "vernac" ->
str "Entry vernac_control is" ++ fnl () ++
- pr_entry Pcoq.Vernac_.vernac_control ++
+ pr_entry Pvernac.Vernac_.vernac_control ++
str "Entry command is" ++ fnl () ++
- pr_entry Pcoq.Vernac_.command ++
+ pr_entry Pvernac.Vernac_.command ++
str "Entry syntax is" ++ fnl () ++
- pr_entry Pcoq.Vernac_.syntax ++
+ pr_entry Pvernac.Vernac_.syntax ++
str "Entry gallina is" ++ fnl () ++
- pr_entry Pcoq.Vernac_.gallina ++
+ pr_entry Pvernac.Vernac_.gallina ++
str "Entry gallina_ext is" ++ fnl () ++
- pr_entry Pcoq.Vernac_.gallina_ext
+ pr_entry Pvernac.Vernac_.gallina_ext
| name -> pr_registered_grammar name
(**********************************************************************)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index dfc51a990..6ef8294df 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -616,7 +616,7 @@ let shrink_body c ty =
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
- Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+ Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
let it_mkLambda_or_LetIn_or_clean t ctx =
let open Context.Rel.Declaration in
diff --git a/printing/ppvernac.ml b/vernac/ppvernac.ml
index 7a34e8027..3655947a5 100644
--- a/printing/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -152,7 +152,7 @@ open Pputils
| SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchAbout sl ->
- keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+ keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
let pr_locality local = if local then keyword "Local" else keyword "Global"
diff --git a/printing/ppvernac.mli b/vernac/ppvernac.mli
index 4aa24bf5d..4aa24bf5d 100644
--- a/printing/ppvernac.mli
+++ b/vernac/ppvernac.mli
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
new file mode 100644
index 000000000..bac882381
--- /dev/null
+++ b/vernac/pvernac.ml
@@ -0,0 +1,56 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pcoq
+
+let uncurry f (x,y) = f x y
+
+let uvernac = create_universe "vernac"
+
+module Vernac_ =
+ struct
+ let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+
+ (* The different kinds of vernacular commands *)
+ let gallina = gec_vernac "gallina"
+ let gallina_ext = gec_vernac "gallina_ext"
+ let command = gec_vernac "command"
+ let syntax = gec_vernac "syntax_command"
+ let vernac_control = gec_vernac "Vernac.vernac_control"
+ let rec_definition = gec_vernac "Vernac.rec_definition"
+ let red_expr = new_entry utactic "red_expr"
+ let hint_info = gec_vernac "hint_info"
+ (* Main vernac entry *)
+ let main_entry = Gram.entry_create "vernac"
+ let noedit_mode = gec_vernac "noedit_command"
+
+ let () =
+ let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
+ let act_eoi = Gram.action (fun _ loc -> None) in
+ let rule = [
+ ([ Symbols.stoken Tok.EOI ], act_eoi);
+ ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
+ ] in
+ uncurry (Gram.extend main_entry) (None, [None, None, rule])
+
+ let command_entry_ref = ref noedit_mode
+ let command_entry =
+ Gram.Entry.of_parser "command_entry"
+ (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
+ end
+
+let main_entry = Vernac_.main_entry
+
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
+let () =
+ register_grammar Stdarg.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
new file mode 100644
index 000000000..9d999793e
--- /dev/null
+++ b/vernac/pvernac.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pcoq
+open Genredexpr
+open Vernacexpr
+
+val uvernac : gram_universe
+
+module Vernac_ :
+ sig
+ val gallina : vernac_expr Gram.entry
+ val gallina_ext : vernac_expr Gram.entry
+ val command : vernac_expr Gram.entry
+ val syntax : vernac_expr Gram.entry
+ val vernac_control : vernac_control Gram.entry
+ val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
+ val noedit_mode : vernac_expr Gram.entry
+ val command_entry : vernac_expr Gram.entry
+ val red_expr : raw_red_expr Gram.entry
+ val hint_info : Typeclasses.hint_info_expr Gram.entry
+ end
+
+(** The main entry: reads an optional vernac command *)
+val main_entry : (Loc.t * vernac_control) option Gram.entry
+
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f001b572a..39c313ac7 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,10 +1,18 @@
+Vernacexpr
+Pvernac
+G_vernac
+G_proofs
Vernacprop
-Proof_using
-Lemmas
Himsg
ExplainErr
-Class
Locality
+Egramml
+Vernacinterp
+Ppvernac
+Proof_using
+Lemmas
+Class
+Egramcoq
Metasyntax
Auto_ind_decl
Search
@@ -20,7 +28,6 @@ Classes
Record
Assumptions
Vernacstate
-Vernacinterp
Mltop
Topfmt
Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 65490bbbc..9a7f59085 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -977,7 +977,7 @@ let vernac_remove_hints ~atts dbs ids =
let vernac_hints ~atts lb h =
let local = enforce_module_locality atts.locality in
- Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
+ Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
let vernac_syntactic_definition ~atts lid x y =
Dumpglob.dump_definition lid false "syndef";
@@ -1971,7 +1971,7 @@ let vernac_load interp fname =
interp x in
let parse_sentence = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Gram.entry_parse Pcoq.main_entry po with
+ match Pcoq.Gram.entry_parse Pvernac.main_entry po with
| Some x -> x
| None -> raise End_of_input) in
let fname =
diff --git a/parsing/vernacexpr.ml b/vernac/vernacexpr.ml
index 6ebf66349..cf0da4de2 100644
--- a/parsing/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -103,14 +103,16 @@ type comment =
| CommentString of string
| CommentInt of int
-type reference_or_constr =
+type reference_or_constr = Hints.reference_or_constr =
| HintsReference of reference
| HintsConstr of constr_expr
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
-type hint_mode =
+type hint_mode = Hints.hint_mode =
| ModeInput (* No evars *)
| ModeNoHeadEvar (* No evar at the head *)
| ModeOutput (* Anything *)
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
{ hint_priority : int option;
@@ -120,14 +122,15 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
type hint_info_expr = Typeclasses.hint_info_expr
[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
-type hints_expr =
- | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
- | HintsImmediate of reference_or_constr list
+type hints_expr = Hints.hints_expr =
+ | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list
+ | HintsImmediate of Hints.reference_or_constr list
| HintsUnfold of reference list
| HintsTransparency of reference list * bool
- | HintsMode of reference * hint_mode list
+ | HintsMode of reference * Hints.hint_mode list
| HintsConstructors of reference list
| HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
type search_restriction =
| SearchInside of reference list
@@ -401,7 +404,7 @@ type nonrec vernac_expr =
(* Commands *)
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * reference list
- | VernacHints of string list * hints_expr
+ | VernacHints of string list * Hints.hints_expr
| VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
onlyparsing_flag
| VernacArguments of reference or_by_notation *