aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--dev/top_printers.ml4
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/q_util.ml44
-rw-r--r--grammar/vernacextend.ml42
-rw-r--r--intf/extend.mli6
-rw-r--r--ltac/g_ltac.ml42
-rw-r--r--ltac/tacentries.ml10
-rw-r--r--parsing/entry.ml30
-rw-r--r--parsing/entry.mli23
-rw-r--r--parsing/parsing.mllib1
-rw-r--r--parsing/pcoq.ml13
-rw-r--r--parsing/pcoq.mli5
13 files changed, 16 insertions, 87 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 390a9f384..aa74cb508 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -194,7 +194,6 @@ Proof_global
Pfedit
Decl_mode
Ppconstr
-Entry
Pcoq
Printer
Pptactic
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9c1971a8..f5599d793 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
extend_vernac_command_grammar ("PrintConstr", 0) None
[GramTerminal "PrintConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+ (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
let _ =
try
@@ -536,7 +536,7 @@ let _ =
extend_vernac_command_grammar ("PrintPureConstr", 0) None
[GramTerminal "PrintPureConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
+ (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
(* Setting printer of unbound global reference *)
open Names
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 0e52dc948..9be6c6bc4 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -42,7 +42,7 @@ let make_act loc act pil =
let make_prod_item = function
| ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
| ExtNonTerminal (g, _) ->
- let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
+ let base s = <:expr< $lid:s$ >> in
mlexpr_of_prod_entry_key base g
let rec make_prod = function
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index c529260e9..05c94394d 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -71,8 +71,8 @@ let rec mlexpr_of_prod_entry_key f = function
| Uentryl (e, l) ->
(** Keep in sync with Pcoq! *)
assert (e = "tactic");
- if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
- else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+ if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >>
+ else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
let rec type_of_user_symbol = function
| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 0d4bec69d..904662ea1 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -106,7 +106,7 @@ let make_prod_item = function
| ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
| ExtNonTerminal (g, id) ->
let nt = type_of_user_symbol g in
- let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
+ let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
<:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
$mlexpr_of_prod_entry_key base g$ >>
diff --git a/intf/extend.mli b/intf/extend.mli
index 381d47dd1..3deb8233f 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -8,6 +8,8 @@
(** Entry keys for constr notations *)
+type 'a entry = 'a Compat.GrammarMake(CLexer).entry
+
type side = Left | Right
type gram_assoc = NonA | RightA | LeftA
@@ -84,8 +86,8 @@ type ('self, 'a) symbol =
| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
| Aself : ('self, 'self) symbol
| Anext : ('self, 'self) symbol
-| Aentry : 'a Entry.t -> ('self, 'a) symbol
-| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol
+| Aentry : 'a entry -> ('self, 'a) symbol
+| Aentryl : 'a entry * int -> ('self, 'a) symbol
| Arules : 'a rules -> ('self, 'a index) symbol
and ('self, _, 'r) rule =
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 1bbdb1779..0c25481d8 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -43,8 +43,6 @@ let tactic_mode = Gram.entry_create "vernac:tactic_command"
let new_entry name =
let e = Gram.entry_create name in
- let entry = Entry.create name in
- let () = Pcoq.set_grammar entry e in
e
let selector = new_entry "vernac:selector"
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 881482081..d0383ffbc 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -43,8 +43,8 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
- else Aentryl (name_of_entry Tactic.tactic_expr, n)
+ if n = 5 then Aentry Tactic.binder_tactic
+ else Aentryl (Tactic.tactic_expr, n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -149,7 +149,7 @@ let rec prod_item_of_symbol lev = function
| Extend.Uentry arg ->
let ArgT.Any tag = arg in
let wit = ExtraArg tag in
- EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+ EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -389,8 +389,8 @@ let create_ltac_quotation name cast (e, l) =
in
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
- | None -> Aentry (name_of_entry e)
- | Some l -> Aentryl (name_of_entry e, l)
+ | None -> Aentry e
+ | Some l -> Aentryl (e, l)
in
(* let level = Some "1" in *)
let level = None in
diff --git a/parsing/entry.ml b/parsing/entry.ml
deleted file mode 100644
index b7c6c23fa..000000000
--- a/parsing/entry.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Errors
-open Util
-
-type 'a t = string
-
-(** Entries are registered with a unique name *)
-
-let entries = ref String.Set.empty
-
-let create name =
- let () =
- if String.Set.mem name !entries then
- anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
- in
- let () = entries := String.Set.add name !entries in
- name
-
-let unsafe_of_name name =
- assert (String.Set.mem name !entries);
- name
-
-let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
deleted file mode 100644
index 4c73fe204..000000000
--- a/parsing/entry.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Typed grammar entries *)
-
-type 'a t
-(** Typed grammar entries. We need to defined them here so that they are
- marshallable and defined before the Pcoq.Gram module. They are basically
- unique names. They should be kept synchronized with the {!Pcoq} entries. *)
-
-val create : string -> 'a t
-(** Create an entry. They should be synchronized with the entries defined in
- {!Pcoq}. *)
-
-(** {5 Meta-programming} *)
-
-val repr : 'a t -> string
-val unsafe_of_name : string -> 'a t
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index b052b6ee6..0e1c79c91 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
Tok
Compat
CLexer
-Entry
Pcoq
Egramml
Egramcoq
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 70bcf1def..a7f7ad7bc 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -215,18 +215,9 @@ let get_univ u =
(** A table associating grammar to entries *)
let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
-let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
- Obj.magic (String.Map.find (Entry.repr e) !gtable)
-
-let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
- assert (not (String.Map.mem (Entry.repr e) !gtable));
- gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
-
let new_entry u s =
let ename = u ^ ":" ^ s in
- let entry = Entry.create ename in
let e = Gram.entry_create ename in
- let () = set_grammar entry e in
e
let make_gen_entry u s = new_entry u s
@@ -689,10 +680,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
| Aself -> Symbols.sself
| Anext -> Symbols.snext
| Aentry e ->
- let e = get_grammar e in
Symbols.snterm (Gram.Entry.obj (weaken_entry e))
| Aentryl (e, n) ->
- let e = get_grammar e in
Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
| Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
@@ -726,8 +715,6 @@ let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
unsafe_grammar_extend e reinit ext
-let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-
let list_entry_names () = []
let epsilon_value f e =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 372350414..70eb21106 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Genredexpr
(** The parser of Coq *)
-module Gram : Compat.GrammarSig
+module Gram : module type of Compat.GrammarMake(CLexer)
(** The parser of Coq is built from three kinds of rule declarations:
@@ -128,7 +128,6 @@ val uconstr : gram_universe
val utactic : gram_universe
val uvernac : gram_universe
-val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
@@ -234,8 +233,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry
val get_command_entry : unit -> vernac_expr Gram.entry
val set_command_entry : vernac_expr Gram.entry -> unit
-val name_of_entry : 'a Gram.entry -> 'a Entry.t
-
val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** Binding general entry keys to symbols *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:33:05 +0000