aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--parsing/egramcoq.ml4
-rw-r--r--printing/pptactic.ml2
-rw-r--r--tactics/tacenv.ml3
-rw-r--r--tactics/tacenv.mli7
-rw-r--r--tactics/tacintern.ml2
-rw-r--r--tactics/tacinterp.ml19
-rw-r--r--tactics/tacsubst.ml2
-rw-r--r--toplevel/metasyntax.ml15
9 files changed, 33 insertions, 23 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 6d10ef9d51..05e7ea1a3b 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -294,7 +294,7 @@ and 'a gen_tactic_expr =
(* For ML extensions *)
| TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
(* For syntax extensions *)
- | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list
+ | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list
constraint 'a = <
term:'t;
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 2bc5b0f83f..bd9bacbc60 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -286,9 +286,9 @@ let add_tactic_entry kn tg =
(** 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
- (id, Tacexp (Genarg.out_gen wit arg))
+ Tacexp (Genarg.out_gen wit arg)
else
- (id, TacGeneric arg)
+ TacGeneric arg
in
let l = List.map2 map l types in
(TacAlias (loc,kn,l):raw_tactic_expr)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4cb7e9fb38..50a543968a 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1201,7 +1201,7 @@ module Make
| TacML (loc,s,l) ->
pr_with_comments loc (pr.pr_extend 1 s l), lcall
| TacAlias (loc,kn,l) ->
- pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+ pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
)
in
if prec_less prec inherited then strm
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index d7ab2d71ec..c7339acea7 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -15,9 +15,10 @@ open Tacexpr
(** Tactic notations (TacAlias) *)
type alias = KerName.t
+type alias_tactic = Id.t list * glob_tactic_expr
let alias_map = Summary.ref ~name:"tactic-alias"
- (KNmap.empty : glob_tactic_expr KNmap.t)
+ (KNmap.empty : alias_tactic KNmap.t)
let register_alias key tac =
alias_map := KNmap.add key tac !alias_map
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 28fb138817..65fd693435 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -17,10 +17,13 @@ open Tacexpr
type alias = KerName.t
(** Type of tactic alias, used in the [TacAlias] node. *)
-val register_alias : alias -> glob_tactic_expr -> unit
+type alias_tactic = Id.t list * glob_tactic_expr
+(** Contents of a tactic notation *)
+
+val register_alias : alias -> alias_tactic -> unit
(** Register a tactic alias. *)
-val interp_alias : alias -> glob_tactic_expr
+val interp_alias : alias -> alias_tactic
(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
val check_alias : alias -> bool
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 93d64f686d..e6273401dd 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -656,7 +656,7 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,s,l) ->
- let l = List.map (fun (id,a) -> (id,intern_tacarg !strict_check false ist a)) l in
+ let l = List.map (intern_tacarg !strict_check false ist) l in
ist.ltacvars, TacAlias (loc,s,l)
| TacML (loc,opn,l) ->
let _ignore = Tacenv.interp_ml_tactic opn in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1596406c9a..a871815881 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1238,14 +1238,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
eval_tactic ist tac
(* For extensions *)
| TacAlias (loc,s,l) ->
- let body = Tacenv.interp_alias s in
+ let (ids, body) = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
- let interp_vars =
- Ftactic.List.map (fun (x,v) -> interp_tacarg ist v >>= fun v -> Ftactic.return (x,v)) l
- in
- let addvar (x, v) accu = Id.Map.add x v accu in
+ let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
- let lfun = List.fold_right addvar l ist.lfun in
+ let addvar x v accu = Id.Map.add x v accu in
+ let lfun = List.fold_right2 addvar ids l ist.lfun in
let trace = push_trace (loc,LtacNotationCall s) ist in
let ist = {
lfun = lfun;
@@ -1255,12 +1253,19 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
- let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s (List.map snd lr) in
+ let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
Proofview.Trace.name_tactic name (tac lr)
(* spiwack: this use of name_tactic is not robust to a
change of implementation of [Ftactic]. In such a situation,
some more elaborate solution will have to be used. *)
in
+ let tac =
+ let len1 = List.length ids in
+ let len2 = List.length l in
+ if len1 = len2 then tac
+ else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
+ expected " ++ int len1 ++ str ", found " ++ int len2)
+ in
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
| TacML (loc,opn,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 45b2d317c2..754c886205 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -245,7 +245,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
(* For extensions *)
| TacAlias (_,s,l) ->
let s = subst_kn subst s in
- TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_tacarg subst a)) l)
+ TacAlias (dloc,s,List.map (subst_tacarg subst) l)
| TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l)
and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0f96c2b4af..821283e946 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -81,7 +81,7 @@ type tactic_grammar_obj = {
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
tacobj_tacpp : Pptactic.pp_tactic;
- tacobj_body : Tacexpr.glob_tactic_expr
+ tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
}
let check_key key =
@@ -111,9 +111,10 @@ let load_tactic_notation i (_, tobj) =
Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
+ let (ids, body) = tobj.tacobj_body in
{ tobj with
tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
- tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body;
+ tacobj_body = (ids, Tacsubst.subst_tactic subst body);
}
let classify_tactic_notation tacobj = Substitute tacobj
@@ -126,9 +127,9 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
subst_function = subst_tactic_notation;
classify_function = classify_tactic_notation}
-let cons_production_parameter l = function
- | GramTerminal _ -> l
- | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
+let cons_production_parameter = function
+ | GramTerminal _ -> None
+ | GramNonTerminal (_, _, _, id) -> id
let add_tactic_notation (local,n,prods,e) =
let prods = List.map (interp_prod_item n) prods in
@@ -137,7 +138,7 @@ let add_tactic_notation (local,n,prods,e) =
Pptactic.pptac_args = tags;
pptac_prods = (n, List.map make_terminal_status prods);
} in
- let ids = List.fold_left cons_production_parameter [] prods in
+ let ids = List.map_filter cons_production_parameter prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
let parule = {
tacgram_level = n;
@@ -148,7 +149,7 @@ let add_tactic_notation (local,n,prods,e) =
tacobj_local = local;
tacobj_tacgram = parule;
tacobj_tacpp = pprule;
- tacobj_body = tac;
+ tacobj_body = (ids, tac);
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:25:04 +0000