Moving the TacAlias node out of atomic tactics.

3 files changed, 112 insertions, 112 deletions

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)