Moving the TacAlias node out of atomic tactics.

7 files changed, 118 insertions, 125 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index b9c41ae03e..cf8d34d7e7 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -162,9 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
-  (* For syntax extensions *)
-  | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
-
 (** Possible arguments of a tactic definition *)
 
 and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg =
@@ -246,6 +243,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacArg of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg located
   (* For ML extensions *)
   | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
+  (* For syntax extensions *)
+  | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
 
 and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
     Id.t option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c56a5a7004..f47eb1c091 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -274,7 +274,7 @@ let head_is_ident tg = match tg.tacgram_prods with
 
 let add_tactic_entry kn tg =
   let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l = (TacAtom(loc, TacAlias (loc,kn,l)):raw_tactic_expr) in
+  let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
       error "Notation for simple tactic must start with an identifier."
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c183cb1603..e6157793e3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -654,9 +654,6 @@ let rec pr_atom0 = function
 
   (* Main tactic printer *)
 and pr_atom1 = function
-  | TacAlias (loc,kn,l) ->
-      pr_with_comments loc (pr_alias 1 kn (List.map snd l))
-
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 t
   | TacIntroPattern (_::_ as p) ->
@@ -916,10 +913,6 @@ let rec pr_tac inherited tac =
       pr_tac (lcomplete,E) t, lcomplete
   | TacId l ->
       str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
-  | TacAtom (loc,TacAlias (_,kn,l)) ->
-      pr_with_comments loc
-        (pr_alias (level_of inherited) kn (List.map snd l)),
-      latom
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
   | TacArg(_,Tacexp e) -> pr_tac_level (latom,E) e, latom
@@ -938,6 +931,8 @@ let rec pr_tac inherited tac =
   | TacArg (_,a) -> pr_tacarg a, latom
   | TacML (loc,s,l) ->
       pr_with_comments loc (pr_extend 1 s l), lcall
+  | TacAlias (loc,kn,l) ->
+      pr_with_comments loc (pr_alias (level_of inherited) kn (List.map snd l)), latom
   in
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c9a3d093de..4a4368404f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -558,11 +558,6 @@ let rec intern_atomic lf ist x =
       TacInversion (intern_inversion_strength lf ist inv,
         intern_quantified_hypothesis ist hyp)
 
-  (* For extensions *)
-  | TacAlias (loc,s,l) ->
-      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
-      TacAlias (loc,s,l)
-
 and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
 
 and intern_tactic_seq onlytac ist = function
@@ -633,6 +628,11 @@ and intern_tactic_seq onlytac ist = function
   | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
   | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
   | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+
+  (* For extensions *)
+  | TacAlias (loc,s,l) ->
+      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
+      ist.ltacvars, TacAlias (loc,s,l)
   | TacML (loc,opn,l) ->
       let () = Hook.get f_assert_tactic_installed opn in
       ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a3551760b1..e1c53df4da 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1116,6 +1116,108 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
 	   strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
+  | TacAlias (loc,s,l) ->
+      let body = Tacenv.interp_alias s in
+      let rec f x = match genarg_tag x with
+      | QuantHypArgType | RedExprArgType
+      | ConstrWithBindingsArgType
+      | BindingsArgType
+      | OptArgType _ | PairArgType _ -> (** generic handler *)
+        GTac.enter begin fun gl ->
+          let sigma = Proofview.Goal.sigma gl in
+          let env = Proofview.Goal.env gl in
+          let concl = Proofview.Goal.concl gl in
+          let goal = Proofview.Goal.goal gl in
+          let (sigma, arg) = interp_genarg ist env sigma concl goal x in
+          Proofview.V82.tclEVARS sigma <*> GTac.return arg
+        end
+      | _ as tag -> (** Special treatment. TODO: use generic handler  *)
+        GTac.enter begin fun gl ->
+          let sigma = Proofview.Goal.sigma gl in
+          let env = Proofview.Goal.env gl in
+          match tag with
+          | IntOrVarArgType ->
+              GTac.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))
+          | IdentArgType ->
+              GTac.return (value_of_ident (interp_fresh_ident ist env
+                                               (out_gen (glbwit wit_ident) x)))
+          | VarArgType ->
+              GTac.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
+          | GenArgType -> f (out_gen (glbwit wit_genarg) x)
+          | ConstrArgType ->
+              let (sigma,v) =
+                Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl
+              in
+              Proofview.V82.tclEVARS sigma <*>
+              GTac.return v
+          | OpenConstrArgType ->
+              let (sigma,v) =
+                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in
+              Proofview.V82.tclEVARS sigma <*>
+              GTac.return v
+          | ConstrMayEvalArgType ->
+              let (sigma,c_interp) =
+                interp_constr_may_eval ist env sigma
+                  (out_gen (glbwit wit_constr_may_eval) x)
+              in
+              Proofview.V82.tclEVARS sigma <*>
+              GTac.return (Value.of_constr c_interp)
+          | ListArgType ConstrArgType ->
+              let wit = glbwit (wit_list wit_constr) in
+              let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
+                Evd.MonadR.List.map_right
+                  (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c)
+                  (out_gen wit x)
+                  (project gl)
+              end gl in
+              Proofview.V82.tclEVARS sigma <*>
+              GTac.return (in_gen (topwit (wit_list wit_genarg)) l_interp)
+          | ListArgType VarArgType ->
+              let wit = glbwit (wit_list wit_var) in
+              GTac.return (
+                let ans = List.map (mk_hyp_value ist env) (out_gen wit x) in
+                in_gen (topwit (wit_list wit_genarg)) ans
+              )
+          | ListArgType IntOrVarArgType ->
+              let wit = glbwit (wit_list wit_int_or_var) in
+              let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
+              GTac.return (in_gen (topwit (wit_list wit_genarg)) ans)
+          | ListArgType IdentArgType ->
+              let wit = glbwit (wit_list wit_ident) in
+              let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
+              let ans = List.map mk_ident (out_gen wit x) in
+              GTac.return (in_gen (topwit (wit_list wit_genarg)) ans)
+          | ListArgType t  ->
+              GenargTac.app_list (fun y -> f y) x
+          | ExtraArgType _ ->
+              let (>>=) = GTac.bind in
+              (** Special treatment of tactics *)
+              if has_type x (glbwit wit_tactic) then
+                let tac = out_gen (glbwit wit_tactic) x in
+                val_interp ist tac >>= fun v ->
+                GTac.return v
+              else
+                let goal = Proofview.Goal.goal gl in
+                let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
+                Proofview.V82.tclEVARS newsigma <*>
+                GTac.return v
+          | _ -> assert false
+        end
+      in
+      let (>>=) = GTac.bind in
+      let addvar (x, v) accu =
+        f v >>= fun v ->
+        GTac.return (Id.Map.add x v accu)
+      in
+      let tac = GTacList.fold_right addvar l ist.lfun >>= fun lfun ->
+        let trace = push_trace (loc,LtacNotationCall s) ist in
+        let ist = {
+          lfun = lfun;
+          extra = TacStore.set ist.extra f_trace trace; } in
+        val_interp ist body
+      in
+      GTac.run tac (fun v -> tactic_of_value ist v)
+
   | TacML (loc,opn,l) when List.for_all global_genarg l ->
       (* spiwack: a special case for tactics (from TACTIC EXTEND) when
          every argument can be interpreted without a
@@ -1906,108 +2008,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
           hyps
       end
 
-  | TacAlias (loc,s,l) ->
-      let body = Tacenv.interp_alias s in
-      let rec f x = match genarg_tag x with
-      | QuantHypArgType | RedExprArgType
-      | ConstrWithBindingsArgType
-      | BindingsArgType
-      | OptArgType _ | PairArgType _ -> (** generic handler *)
-        GTac.enter begin fun gl ->
-          let sigma = Proofview.Goal.sigma gl in
-          let env = Proofview.Goal.env gl in
-          let concl = Proofview.Goal.concl gl in
-          let goal = Proofview.Goal.goal gl in
-          let (sigma, arg) = interp_genarg ist env sigma concl goal x in
-          Proofview.V82.tclEVARS sigma <*> GTac.return arg
-        end
-      | _ as tag -> (** Special treatment. TODO: use generic handler  *)
-        GTac.enter begin fun gl ->
-          let sigma = Proofview.Goal.sigma gl in
-          let env = Proofview.Goal.env gl in
-          match tag with
-          | IntOrVarArgType ->
-              GTac.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))
-          | IdentArgType ->
-              GTac.return (value_of_ident (interp_fresh_ident ist env
-	                                       (out_gen (glbwit wit_ident) x)))
-          | VarArgType ->
-              GTac.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
-          | GenArgType -> f (out_gen (glbwit wit_genarg) x)
-          | ConstrArgType ->
-              let (sigma,v) =
-                Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl
-              in
-              Proofview.V82.tclEVARS sigma <*>
-	      GTac.return v
-          | OpenConstrArgType ->
-              let (sigma,v) =
-                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in
-              Proofview.V82.tclEVARS sigma <*>
-	      GTac.return v
-          | ConstrMayEvalArgType ->
-              let (sigma,c_interp) =
-                interp_constr_may_eval ist env sigma
-                  (out_gen (glbwit wit_constr_may_eval) x)
-              in
-              Proofview.V82.tclEVARS sigma <*>
-	      GTac.return (Value.of_constr c_interp)
-          | ListArgType ConstrArgType ->
-              let wit = glbwit (wit_list wit_constr) in
-              let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
-                Evd.MonadR.List.map_right
-                  (fun c sigma -> mk_constr_value ist { gl with sigma=sigma } c)
-                  (out_gen wit x)
-                  (project gl)
-              end gl in
-              Proofview.V82.tclEVARS sigma <*>
-              GTac.return (in_gen (topwit (wit_list wit_genarg)) l_interp)
-          | ListArgType VarArgType ->
-              let wit = glbwit (wit_list wit_var) in
-              GTac.return (
-                let ans = List.map (mk_hyp_value ist env) (out_gen wit x) in
-                in_gen (topwit (wit_list wit_genarg)) ans
-              )
-          | ListArgType IntOrVarArgType ->
-              let wit = glbwit (wit_list wit_int_or_var) in
-              let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
-              GTac.return (in_gen (topwit (wit_list wit_genarg)) ans)
-          | ListArgType IdentArgType ->
-              let wit = glbwit (wit_list wit_ident) in
-	      let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
-	      let ans = List.map mk_ident (out_gen wit x) in
-              GTac.return (in_gen (topwit (wit_list wit_genarg)) ans)
-          | ListArgType t  ->
-              GenargTac.app_list (fun y -> f y) x
-          | ExtraArgType _ ->
-              let (>>=) = GTac.bind in
-              (** Special treatment of tactics *)
-              if has_type x (glbwit wit_tactic) then
-                let tac = out_gen (glbwit wit_tactic) x in
-                val_interp ist tac >>= fun v ->
-                GTac.return v
-              else
-                let goal = Proofview.Goal.goal gl in
-                let (newsigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} x in
-                Proofview.V82.tclEVARS newsigma <*>
-                GTac.return v
-          | _ -> assert false
-        end
-      in
-      let (>>=) = GTac.bind in
-      let addvar (x, v) accu =
-        f v >>= fun v ->
-        GTac.return (Id.Map.add x v accu)
-      in
-      let tac = GTacList.fold_right addvar l ist.lfun >>= fun lfun ->
-        let trace = push_trace (loc,LtacNotationCall s) ist in
-        let ist = {
-          lfun = lfun;
-          extra = TacStore.set ist.extra f_trace trace; } in
-        val_interp ist body
-      in
-      GTac.run tac (fun v -> tactic_of_value ist v)
-
 (* Initial call for interpretation *)
 
 let default_ist () =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index f2949ab5e8..288ebc33e9 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -202,11 +202,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacInversion (InversionUsing (c,cl),hyp) ->
       TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
 
-  (* For extensions *)
-  | TacAlias (_,s,l) ->
-      let s = subst_kn subst s in
-      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
-
 and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
   | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
@@ -251,6 +246,11 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
   | TacComplete tac -> TacComplete (subst_tactic subst tac)
   | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a)
+
+  (* For extensions *)
+  | TacAlias (_,s,l) ->
+      let s = subst_kn subst s in
+      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
   | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_genarg subst) l)
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e40e8a73a9..ae8e1f532d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1194,9 +1194,8 @@ let explain_ltac_call_trace last trace loc =
            pr_enum pr_call calls ++ strbrk kind_of_last_call)
 
 let skip_extensions trace =
+  (** FIXME: handle TacAlias & TacML *)
   let rec aux = function
-  | (_,Proof_type.LtacAtomCall
-      (Tacexpr.TacAlias _) as tac) :: tail -> [tac]
   | _ :: tail -> aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))