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.

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)