Separation of concern in TacAlias API.

The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.

5 files changed, 21 insertions, 12 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index d7ab2d71e..c7339acea 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 28fb13881..65fd69343 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 93d64f686..e6273401d 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 1596406c9..a87181588 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 45b2d317c..754c88620 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)