aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml436
-rw-r--r--grammar/vernacextend.ml48
-rw-r--r--intf/extend.mli16
-rw-r--r--ltac/extraargs.ml410
-rw-r--r--ltac/g_ltac.ml42
-rw-r--r--ltac/tacentries.ml173
-rw-r--r--ltac/tacentries.mli40
-rw-r--r--parsing/pcoq.ml100
-rw-r--r--parsing/pcoq.mli4
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--printing/pptactic.ml15
-rw-r--r--printing/pptactic.mli1
12 files changed, 201 insertions, 206 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 2ef30f299b..19b6e1b5f6 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -45,26 +45,30 @@ let make_fun_clauses loc s l =
let map c = Compat.make_fun loc [make_clause c] in
mlexpr_of_list map l
+let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+ let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
+ <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+| Uentryl (e, l) ->
+ assert (e = "tactic");
+ let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+ <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
+
let make_prod_item = function
- | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+ | ExtTerminal s -> <:expr< Tacentries.TacTerm $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
- <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
- $mlexpr_of_prod_entry_key base g$ >>
+ <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
let mlexpr_of_clause cl =
mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
-let make_one_printing_rule (pt,_,e) =
- let level = mlexpr_of_int 0 in (* only level 0 supported here *)
- let loc = MLast.loc_of_expr e in
- let prods = mlexpr_of_list make_prod_item pt in
- <:expr< { Pptactic.pptac_level = $level$;
- pptac_prods = $prods$ } >>
-
-let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
-
(** Special treatment of constr entries *)
let is_constr_gram = function
| ExtTerminal _ -> false
@@ -118,15 +122,13 @@ let declare_tactic loc s c cl = match cl with
TacML tactic. *)
let entry = mlexpr_of_string s in
let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
- let pp = make_printing_rule cl in
let gl = mlexpr_of_clause cl in
let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
declare_str_items loc
[ <:str_item< do {
try do {
Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
- Mltop.declare_cache_obj $obj$ $plugin_name$;
- Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); }
+ Mltop.declare_cache_obj $obj$ $plugin_name$; }
with [ e when Errors.noncritical e ->
Pp.msg_warning
(Pp.app
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index aedaead71a..0d4bec69d5 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -102,6 +102,14 @@ let make_fun_classifiers loc s c l =
let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
mlexpr_of_list (fun x -> x) cl
+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
+ <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+ $mlexpr_of_prod_entry_key base g$ >>
+
let mlexpr_of_clause cl =
let mkexpr { r_head = a; r_patt = b; } = match a with
| None -> mlexpr_of_list make_prod_item b
diff --git a/intf/extend.mli b/intf/extend.mli
index 10713745e4..381d47dd18 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -53,14 +53,14 @@ type simple_constr_prod_entry_key =
(** {5 AST for user-provided entries} *)
-type user_symbol =
-| Ulist1 : user_symbol -> user_symbol
-| Ulist1sep : user_symbol * string -> user_symbol
-| Ulist0 : user_symbol -> user_symbol
-| Ulist0sep : user_symbol * string -> user_symbol
-| Uopt : user_symbol -> user_symbol
-| Uentry : string -> user_symbol
-| Uentryl : string * int -> user_symbol
+type 'a user_symbol =
+| Ulist1 of 'a user_symbol
+| Ulist1sep of 'a user_symbol * string
+| Ulist0 of 'a user_symbol
+| Ulist0sep of 'a user_symbol * string
+| Uopt of 'a user_symbol
+| Uentry of 'a
+| Uentryl of 'a * int
(** {5 Type-safe grammar extension} *)
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index fbae17bafc..0bddcc9fdd 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -40,6 +40,16 @@ let () =
let inject (loc, v) = Tacexpr.Tacexp v in
Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+(** Backward-compatible tactic notation entry names *)
+
+let () =
+ let register name entry = Tacentries.register_tactic_notation_entry name entry in
+ register "hyp" wit_var;
+ register "simple_intropattern" wit_intro_pattern;
+ register "integer" wit_integer;
+ register "reference" wit_ref;
+ ()
+
(* Rewriting orientation *)
let _ = Metasyntax.add_token_obj "<-"
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index fe750f429f..df499a2c9c 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -405,7 +405,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation
[
let l = Locality.LocalityFixme.consume () in
let n = Option.default 0 n in
- Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e)
+ Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e
]
END
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 46e48c6953..f94f84a73b 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -23,6 +23,9 @@ type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
| TacNonTerm of Loc.t * 'a * Names.Id.t
+type raw_argument = string * string option
+type argument = Genarg.ArgT.any Extend.user_symbol
+
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
@@ -46,12 +49,6 @@ let atactic n =
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
-let try_get_entry u s =
- let open Extend in
- (** Order the effects: get_entry can raise Not_found *)
- let TypedEntry (typ, e) = get_entry u s in
- EntryName (typ, Aentry (name_of_entry e))
-
(** Quite ad-hoc *)
let get_tacentry n m =
let open Extend in
@@ -91,13 +88,12 @@ let rec parse_user_entry s sep =
let n = Char.code s.[6] - 48 in
Uentryl ("tactic", n)
else
- let s = match s with "hyp" -> "var" | _ -> s in
Uentry s
let arg_list = function Rawwit t -> Rawwit (ListArg t)
let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-let interp_entry_name up_level s sep =
+let interp_entry_name interp symb =
let open Extend in
let rec eval = function
| Ulist1 e ->
@@ -115,19 +111,10 @@ let interp_entry_name up_level s sep =
| Uopt e ->
let EntryName (t, g) = eval e in
EntryName (arg_opt t, Aopt g)
- | Uentry s ->
- begin
- try try_get_entry uprim s with Not_found ->
- try try_get_entry uconstr s with Not_found ->
- try try_get_entry utactic s with Not_found ->
- error ("Unknown entry "^s^".")
- end
- | Uentryl (s, n) ->
- (** FIXME: do better someday *)
- assert (String.equal s "tactic");
- get_tacentry n up_level
+ | Uentry s -> interp s None
+ | Uentryl (s, n) -> interp s (Some n)
in
- eval (parse_user_entry s sep)
+ eval symb
(**********************************************************************)
(** Grammar declaration for Tactic Notation (Coq level) *)
@@ -150,21 +137,6 @@ type tactic_grammar = {
tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
}
-(** ML Tactic grammar extensions *)
-
-let add_ml_tactic_entry (name, prods) =
- let entry = Tactic.simple_tactic in
- let mkact i loc l : Tacexpr.raw_tactic_expr =
- let open Tacexpr in
- let entry = { mltac_name = name; mltac_index = i } in
- let map arg = TacGeneric arg in
- TacML (loc, entry, List.map map l)
- in
- let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
- synchronize_level_positions ();
- grammar_extend entry None (None, [(None, None, List.rev rules)]);
- 1
-
(* Declaration of the tactic grammar rule *)
let head_is_ident tg = match tg.tacgram_prods with
@@ -173,7 +145,7 @@ let head_is_ident tg = match tg.tacgram_prods with
(** Tactic grammar extensions *)
-let add_tactic_entry (kn, tg) =
+let add_tactic_entry (kn, ml, tg) =
let open Tacexpr in
let entry, pos = get_tactic_entry tg.tacgram_level in
let mkact loc l =
@@ -185,7 +157,7 @@ let add_tactic_entry (kn, tg) =
let map arg t =
(** HACK to handle especially the tactic(...) entry *)
let wit = Genarg.rawwit Constrarg.wit_tactic in
- if Genarg.argument_type_eq t (Genarg.unquote wit) then
+ if Genarg.argument_type_eq t (Genarg.unquote wit) && not ml then
Tacexp (Genarg.out_gen wit arg)
else
TacGeneric arg
@@ -205,24 +177,42 @@ let add_tactic_entry (kn, tg) =
let tactic_grammar =
create_grammar_command "TacticGrammar" add_tactic_entry
-let ml_tactic_grammar =
- create_grammar_command "MLTacticGrammar" add_ml_tactic_entry
-
-let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn)
-let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
+let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn)
(**********************************************************************)
(* Tactic Notation *)
+let entry_names = ref String.Map.empty
+
+let register_tactic_notation_entry name entry =
+ let entry = match entry with
+ | ExtraArg arg -> ArgT.Any arg
+ | _ -> assert false
+ in
+ entry_names := String.Map.add name entry !entry_names
+
let interp_prod_item lev = function
| TacTerm s -> GramTerminal s
| TacNonTerm (loc, (nt, sep), _) ->
- let EntryName (etyp, e) = interp_entry_name lev nt sep in
- GramNonTerminal (loc, etyp, e)
-
-let make_terminal_status = function
- | GramTerminal s -> Some s
- | GramNonTerminal _ -> None
+ let symbol = parse_user_entry nt sep in
+ let interp s = function
+ | None ->
+ let ArgT.Any arg =
+ if String.Map.mem s !entry_names then
+ String.Map.find s !entry_names
+ else match ArgT.name s with
+ | None -> error ("Unknown entry "^s^".")
+ | Some arg -> arg
+ in
+ let wit = ExtraArg arg in
+ EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+ | Some n ->
+ (** FIXME: do better someday *)
+ assert (String.equal s "tactic");
+ get_tacentry n lev
+ in
+ let EntryName (etyp, e) = interp_entry_name interp symbol in
+ GramNonTerminal (loc, etyp, e)
let make_fresh_key =
let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -243,8 +233,13 @@ type tactic_grammar_obj = {
tacobj_key : KerName.t;
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
- tacobj_tacpp : Pptactic.pp_tactic;
tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+ tacobj_forml : bool;
+}
+
+let pprule pa = {
+ Pptactic.pptac_level = pa.tacgram_level;
+ pptac_prods = pa.tacgram_prods;
}
let check_key key =
@@ -256,22 +251,22 @@ let cache_tactic_notation (_, tobj) =
let key = tobj.tacobj_key in
let () = check_key key in
Tacenv.register_alias key tobj.tacobj_body;
- extend_tactic_grammar key tobj.tacobj_tacgram;
- Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
+ extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram;
+ Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)
let open_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
if Int.equal i 1 && not tobj.tacobj_local then
- extend_tactic_grammar key tobj.tacobj_tacgram
+ extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
let load_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
let () = check_key key in
(** Only add the printing and interpretation rules. *)
Tacenv.register_alias key tobj.tacobj_body;
- Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
+ Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
if Int.equal i 1 && not tobj.tacobj_local then
- extend_tactic_grammar key tobj.tacobj_tacgram
+ extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
let (ids, body) = tobj.tacobj_body in
@@ -294,14 +289,7 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, _, id) -> Some id
-let add_tactic_notation (local,n,prods,e) =
- let ids = List.map_filter cons_production_parameter prods in
- let prods = List.map (interp_prod_item n) prods in
- let pprule = {
- Pptactic.pptac_level = n;
- pptac_prods = prods;
- } in
- let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+let add_glob_tactic_notation local n prods forml ids tac =
let parule = {
tacgram_level = n;
tacgram_prods = prods;
@@ -310,21 +298,20 @@ let add_tactic_notation (local,n,prods,e) =
tacobj_key = make_fresh_key ();
tacobj_local = local;
tacobj_tacgram = parule;
- tacobj_tacpp = pprule;
tacobj_body = (ids, tac);
+ tacobj_forml = forml;
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
+let add_tactic_notation local n prods e =
+ let ids = List.map_filter cons_production_parameter prods in
+ let prods = List.map (interp_prod_item n) prods in
+ let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
+ add_glob_tactic_notation local n prods false ids tac
+
(**********************************************************************)
(* ML Tactic entries *)
-type ml_tactic_grammar_obj = {
- mltacobj_name : Tacexpr.ml_tactic_name;
- (** ML-side unique name *)
- mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
- (** Grammar rules generating the ML tactic. *)
-}
-
exception NonEmptyArgument
(** ML tactic notations whose use can be restricted to an identifier are added
@@ -359,27 +346,33 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let cache_ml_tactic_notation (_, obj) =
- extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
-
-let open_ml_tactic_notation i obj =
- if Int.equal i 1 then cache_ml_tactic_notation obj
-
-let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
- declare_object { (default_object "MLTacticGrammar") with
- open_function = open_ml_tactic_notation;
- cache_function = cache_ml_tactic_notation;
- classify_function = (fun o -> Substitute o);
- subst_function = (fun (_, o) -> o);
- }
-
let add_ml_tactic_notation name prods =
- let obj = {
- mltacobj_name = name;
- mltacobj_prod = prods;
- } in
- Lib.add_anonymous_leaf (inMLTacticGrammar obj);
- extend_atomic_tactic name prods
+ let interp_prods = function
+ | TacTerm s -> None, GramTerminal s
+ | TacNonTerm (loc, symb, id) ->
+ let interp (ArgT.Any tag) lev = match lev with
+ | None ->
+ let wit = ExtraArg tag in
+ EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit)))
+ | Some lev ->
+ assert (coincide (ArgT.repr tag) "tactic" 0);
+ EntryName (Rawwit Constrarg.wit_tactic, atactic lev)
+ in
+ let EntryName (etyp, e) = interp_entry_name interp symb in
+ Some id, GramNonTerminal (loc, etyp, e)
+ in
+ let prods = List.map (fun p -> List.map interp_prods p) prods in
+ let iter i prods =
+ let open Tacexpr in
+ let (ids, prods) = List.split prods in
+ let ids = List.map_filter (fun x -> x) ids in
+ let entry = { mltac_name = name; mltac_index = i } in
+ let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
+ let tac = TacML (Loc.ghost, entry, List.map map ids) in
+ add_glob_tactic_notation false 0 prods true ids tac
+ in
+ List.iteri iter prods;
+ extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods)
(**********************************************************************)
(** Ltac quotations *)
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 0f4bb2530e..7586bff92f 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -6,25 +6,51 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Ltac toplevel command entries. *)
+
open Vernacexpr
open Tacexpr
+(** {5 Tactic Definitions} *)
+
+val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit
+(** Adds new Ltac definitions to the environment. *)
+
+(** {5 Tactic Notations} *)
+
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
| TacNonTerm of Loc.t * 'a * Names.Id.t
-(** Adding a tactic notation in the environment *)
+type raw_argument = string * string option
+(** An argument type as provided in Tactic notations, i.e. a string like
+ "ne_foo_list_opt" together with a separator that only makes sense in the
+ "_sep" cases. *)
+
+type argument = Genarg.ArgT.any Extend.user_symbol
+(** A fully resolved argument type given as an AST with generic arguments on the
+ leaves. *)
val add_tactic_notation :
- locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr ->
- unit
+ locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
+ raw_tactic_expr -> unit
+(** [add_tactic_notation local level prods expr] adds a tactic notation in the
+ environment at level [level] with locality [local] made of the grammar
+ productions [prods] and returning the body [expr] *)
+
+val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
+(** Register an argument under a given entry name for tactic notations. When
+ translating [raw_argument] into [argument], atomic names will be first
+ looked up according to names registered through this function and fallback
+ to finding an argument by name (as in {!Genarg}) if there is none
+ matching. *)
val add_ml_tactic_notation : ml_tactic_name ->
- Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
-
-val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
+ argument grammar_tactic_prod_item_expr list list -> unit
+(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
+ ML-side macro. *)
-(** {5 Adding tactic quotations} *)
+(** {5 Tactic Quotations} *)
val create_ltac_quotation : string ->
('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 802c24eef4..e60b470fdf 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,8 +12,6 @@ open Errors
open Util
open Extend
open Genarg
-open Stdarg
-open Constrarg
open Tok (* necessary for camlp4 *)
(** The parser of Coq *)
@@ -53,8 +51,6 @@ end
(** Grammar entries with associated types *)
type grammar_object = Gramobj.grammar_object
-type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> typed_entry
-let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
let weaken_entry x = Gramobj.weaken_entry x
(** Grammar extensions *)
@@ -177,12 +173,11 @@ let parse_string f x =
type gram_universe = string
-let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
+let utables : (string, unit) Hashtbl.t =
Hashtbl.create 97
let create_universe u =
- let table = Hashtbl.create 97 in
- let () = Hashtbl.add utables u table in
+ let () = Hashtbl.add utables u () in
u
let uprim = create_universe "prim"
@@ -194,14 +189,6 @@ let get_univ u =
if Hashtbl.mem utables u then u
else raise Not_found
-let get_utable u =
- try Hashtbl.find utables u
- with Not_found -> assert false
-
-let get_entry u s =
- let utab = get_utable u in
- Hashtbl.find utab s
-
(** A table associating grammar to entries *)
let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
@@ -212,15 +199,14 @@ 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 etyp u s =
- let utab = get_utable u in
+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
- Hashtbl.add utab s (TypedEntry (etyp, e)); e
+ e
-let make_gen_entry u rawwit s = new_entry rawwit u s
+let make_gen_entry u s = new_entry u s
module GrammarObj =
struct
@@ -235,36 +221,32 @@ let register_grammar = Grammar.register0
let genarg_grammar = Grammar.obj
let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
- let utab = get_utable u in
- if Hashtbl.mem utab s then
- failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists")
- else
- let e = new_entry etyp u s in
- let Rawwit t = etyp in
- let () = Grammar.register0 t e in
- e
+ let e = new_entry u s in
+ let Rawwit t = etyp in
+ let () = Grammar.register0 t e in
+ e
(* Initial grammar entries *)
module Prim =
struct
- let gec_gen x = make_gen_entry uprim x
+ let gec_gen n = make_gen_entry uprim n
(* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic or vernac extensions *)
- let preident = gec_gen (rawwit wit_pre_ident) "preident"
- let ident = gec_gen (rawwit wit_ident) "ident"
- let natural = gec_gen (rawwit wit_int) "natural"
- let index = gec_gen (rawwit wit_int) "index"
- let integer = gec_gen (rawwit wit_int) "integer"
+ let preident = gec_gen "preident"
+ let ident = gec_gen "ident"
+ let natural = gec_gen "natural"
+ let index = gec_gen "index"
+ let integer = gec_gen "integer"
let bigint = Gram.entry_create "Prim.bigint"
- let string = gec_gen (rawwit wit_string) "string"
- let reference = make_gen_entry uprim (rawwit wit_ref) "reference"
+ let string = gec_gen "string"
+ let reference = make_gen_entry uprim "reference"
let by_notation = Gram.entry_create "by_notation"
let smart_global = Gram.entry_create "smart_global"
(* parsed like ident but interpreted as a term *)
- let var = gec_gen (rawwit wit_var) "var"
+ let var = gec_gen "var"
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
@@ -286,7 +268,7 @@ module Prim =
module Constr =
struct
- let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
+ let gec_constr = make_gen_entry uconstr
(* Entries that can be referred via the string -> Gram.entry table *)
let constr = gec_constr "constr"
@@ -294,9 +276,9 @@ module Constr =
let constr_eoi = eoi_entry constr
let lconstr = gec_constr "lconstr"
let binder_constr = gec_constr "binder_constr"
- let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
- let global = make_gen_entry uconstr (rawwit wit_ref) "global"
- let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
+ let ident = make_gen_entry uconstr "ident"
+ let global = make_gen_entry uconstr "global"
+ let sort = make_gen_entry uconstr "sort"
let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
@@ -324,32 +306,32 @@ module Tactic =
(* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
+ make_gen_entry utactic "open_constr"
let constr_with_bindings =
- make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
+ make_gen_entry utactic "constr_with_bindings"
let bindings =
- make_gen_entry utactic (rawwit wit_bindings) "bindings"
+ make_gen_entry utactic "bindings"
let hypident = Gram.entry_create "hypident"
- let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
- let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval"
+ let constr_may_eval = make_gen_entry utactic "constr_may_eval"
+ let constr_eval = make_gen_entry utactic "constr_eval"
let uconstr =
- make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
+ make_gen_entry utactic "uconstr"
let quantified_hypothesis =
- make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis"
- let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var"
- let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
+ make_gen_entry utactic "quantified_hypothesis"
+ let int_or_var = make_gen_entry utactic "int_or_var"
+ let red_expr = make_gen_entry utactic "red_expr"
let simple_intropattern =
- make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
+ make_gen_entry utactic "simple_intropattern"
let clause_dft_concl =
- make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause"
+ make_gen_entry utactic "clause"
(* Main entries for ltac *)
let tactic_arg = Gram.entry_create "tactic:tactic_arg"
- let tactic_expr = make_gen_entry utactic (rawwit wit_tactic) "tactic_expr"
- let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic"
+ let tactic_expr = make_gen_entry utactic "tactic_expr"
+ let binder_tactic = make_gen_entry utactic "binder_tactic"
- let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
+ let tactic = make_gen_entry utactic "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
@@ -593,9 +575,7 @@ let compute_entry adjust forpat = function
| ETReference -> weaken_entry Constr.global, None, false
| ETPattern -> weaken_entry Constr.pattern, None, false
| ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
- | ETOther (u,n) ->
- let e = get_entry u n in
- object_of_typed_entry e, None, true
+ | ETOther (u,n) -> assert false
(* This computes the name of the level where to add a new rule *)
let interp_constr_entry_key forpat level =
@@ -725,11 +705,7 @@ let grammar_extend e reinit ext =
let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-let list_entry_names () =
- let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
- let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
- let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
- Hashtbl.fold add_entry (get_utable utactic) ans
+let list_entry_names () = []
let epsilon_value f e =
let r = Rule (Next (Stop, e), fun x _ -> f x) in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index afe8889096..d320520015 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,10 +268,6 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** Binding general entry keys to symbols *)
-type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-
-val get_entry : gram_universe -> string -> typed_entry
-
(** Recover the list of all known tactic notation entries. *)
val list_entry_names : unit -> (string * argument_type) list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8baa668c7b..5e6a3eac73 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1126,7 +1126,7 @@ let type_uconstr ?(flags = constr_flags)
ltac_constrs = closure.typed;
ltac_uconstrs = closure.untyped;
ltac_idents = closure.idents;
- ltac_genargs = ist.Geninterp.lfun;
+ ltac_genargs = Id.Map.empty;
} in
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 19536d9f83..631cb4c577 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -33,16 +33,9 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-(* ML Extensions *)
-let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
- Hashtbl.create 17
-
(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
-let declare_ml_tactic_pprule key pt =
- Hashtbl.add prtac_tab key pt
-
let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -371,14 +364,6 @@ module Make
pr_sequence (fun x -> x) l
let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
- try
- let pp_rules = Hashtbl.find prtac_tab s in
- let pp = pp_rules.(i) in
- let args = List.map_filter filter_arg pp.pptac_prods in
- let () = if not (List.for_all2eq check args l) then raise Not_found in
- let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
- if pp.pptac_level > lev then surround p else p
- with Not_found ->
let name =
str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
str "@" ++ int i
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 31a5a5d4a8..1608cae751 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -48,7 +48,6 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
(** The default pretty-printers produce {!Pp.std_ppcmds} that are
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 02:52:43 +0000