diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 3 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 7 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 8 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 1 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
9 files changed, 27 insertions, 10 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 0421ad7ce..e91e66696 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -186,6 +186,7 @@ let declare_tactic loc s c cl = match cl with let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in + let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in let name = mlexpr_of_string name in let tac = (** Special handling of tactics without arguments: such tactics do not do @@ -200,7 +201,7 @@ let declare_tactic loc s c cl = match cl with (** Arguments are not passed directly to the ML tactic in the TacML node, the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in + let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7b9ad3136..f0377cff9 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -101,6 +101,11 @@ type ml_tactic_name = { mltac_tactic : string; } +type ml_tactic_entry = { + mltac_name : ml_tactic_name; + mltac_index : int; +} + (** Composite types *) (** In globalize tactics, we need to keep the initial [constr_expr] to recompute @@ -287,7 +292,7 @@ and 'a gen_tactic_expr = | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located (* For ML extensions *) - | TacML of Loc.t * ml_tactic_name * 'l generic_argument list + | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list (* For syntax extensions *) | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 01194c60d..d9eb5d412 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -258,8 +258,12 @@ type all_grammar_command = let add_ml_tactic_entry name prods = let entry = weaken_entry Tactic.simple_tactic in - let mkact loc l : raw_tactic_expr = Tacexpr.TacML (loc, name, List.map snd l) in - let rules = List.map (make_rule mkact) prods in + let mkact i loc l : raw_tactic_expr = + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + TacML (loc, entry, List.map snd 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 diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2f9e8509c..72ebfae48 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -143,6 +143,10 @@ let closed_term_ast l = mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let tacname = { + mltac_name = tacname; + mltac_index = 0; + } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f8264e5af..bc837d81d 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1250,7 +1250,7 @@ module Make | TacArg (_,a) -> pr_tacarg a, latom | TacML (loc,s,l) -> - pr_with_comments loc (pr.pr_extend 1 s l), lcall + pr_with_comments loc (pr.pr_extend 1 s.mltac_name l), lcall | TacAlias (loc,kn,l) -> pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom ) diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cb20fc930..9d8b9a9d5 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -58,7 +58,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic s = +let interp_ml_tactic { mltac_name = s } = try MLTacMap.find s !tac_tab with Not_found -> diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4c..72b1ca90f 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -51,5 +51,5 @@ type ml_tactic = val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 4b03ff249..8de804d6d 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -159,6 +159,7 @@ let flatten_contravariant_conj flags ist = let constructor i = let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in + let name = { Tacexpr.mltac_name = name; mltac_index = 0 } in let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in Tacexpr.TacML (Loc.ghost, name, [i]) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 161cf8247..968f72486 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -137,13 +137,15 @@ type ml_tactic_grammar_obj = { (** ML tactic notations whose use can be restricted to an identifier are added as true Ltac entries. *) let extend_atomic_tactic name entries = - let add_atomic (id, args) = match args with + let add_atomic i (id, args) = match args with | None -> () | Some args -> - let body = Tacexpr.TacML (Loc.ghost, name, args) in + let open Tacexpr in + let entry = { mltac_name = name; mltac_index = i } in + let body = TacML (Loc.ghost, entry, args) in Tacenv.register_ltac false false (Names.Id.of_string id) body in - List.iter add_atomic entries + List.iteri add_atomic entries let cache_ml_tactic_notation (_, obj) = extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod |