Clean-up : removal of Proof_type.tactic_expr

 This instance of gen_tactic_expr was used only to decorate
 tactics via Refiner.abstract_tactics and alii, but these
 expressions are now ignored by the new proof-engine (no "info"...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 56 insertions, 85 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 748b608b4b..926e65d29a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1017,7 +1017,7 @@ let auto_unif_flags = {
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let h_clenv_refine ev c clenv =
-  Refiner.abstract_tactic (TacApply (true,ev,[c,NoBindings],None))
+  Refiner.abstract_tactic
     (Clenvtac.clenv_refine ev clenv)
 
 let unify_resolve_nodelta (c,clenv) gl =
@@ -1355,7 +1355,7 @@ let gen_trivial ?(debug=Off) lems = function
   | Some l -> trivial ~debug lems l
 
 let h_trivial ?(debug=Off) lems l =
-  Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
+  Refiner.abstract_tactic
     (gen_trivial ~debug lems l)
 
 (**************************************************************************)
@@ -1439,5 +1439,5 @@ let gen_auto ?(debug=Off) n lems dbnames =
 let inj_or_var = Option.map (fun n -> ArgArg n)
 
 let h_auto ?(debug=Off) n lems l =
-  Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
+  Refiner.abstract_tactic
     (gen_auto ~debug n lems l)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 32acc5af57..a25a370922 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -123,13 +123,13 @@ let decompose_or c gls =
     c gls
 
 let h_decompose l c =
-  Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
+  Refiner.abstract_tactic (decompose_these c l)
 
 let h_decompose_or c =
-  Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
+  Refiner.abstract_tactic (decompose_or c)
 
 let h_decompose_and c =
-  Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
+  Refiner.abstract_tactic (decompose_and c)
 
 (* The tactic Double performs a double induction *)
 
@@ -175,6 +175,6 @@ let double_ind h1 h2 gls =
              ([],[]) (mkVar id)))) gls
 
 let h_double_induction h1 h2 =
-  Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)
+  Refiner.abstract_tactic (double_ind h1 h2)
 
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 5329029a81..89d2a85d8b 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -73,7 +73,7 @@ let solveNoteqBranch side =
       (onLastHypId (fun id -> Extratactics.h_discrHyp id)))
 
 let h_solveNoteqBranch side =
-  Refiner.abstract_extended_tactic "solveNoteqBranch" []
+  Refiner.abstract_extended_tactic
     (solveNoteqBranch side)
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b68b6c545e..25106d1ef9 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -14,125 +14,97 @@ open Locus
 open Misctypes
 
 (* Basic tactics *)
-let h_intro_move x y =
-  abstract_tactic (TacIntroMove (x, y)) (intro_move x y)
+let h_intro_move x y = abstract_tactic (intro_move x y)
 let h_intro x        = h_intro_move (Some x) MoveLast
-let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
-let h_assumption     = abstract_tactic TacAssumption assumption
-let h_exact c        = abstract_tactic (TacExact c) (exact_check c)
-let h_exact_no_check c =
-  abstract_tactic (TacExactNoCheck c) (exact_no_check c)
-let h_vm_cast_no_check c =
-  abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
-let h_apply simple ev cb =
-  abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
+let h_intros_until x = abstract_tactic (intros_until x)
+let h_assumption     = abstract_tactic assumption
+let h_exact c        = abstract_tactic (exact_check c)
+let h_exact_no_check c = abstract_tactic (exact_no_check c)
+let h_vm_cast_no_check c = abstract_tactic (vm_cast_no_check c)
+let h_apply simple ev cb = abstract_tactic
     (apply_with_bindings_gen simple ev cb)
-let h_apply_in simple ev cb (id,ipat as inhyp) =
-  abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
-    (apply_in simple ev id cb ipat)
-let h_elim ev cb cbo    =
-  abstract_tactic (TacElim (ev,cb,cbo))
-    (elim ev cb cbo)
-let h_elim_type c    = abstract_tactic (TacElimType c) (elim_type c)
-let h_case ev cb     = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb)
-let h_case_type c    = abstract_tactic (TacCaseType c) (case_type c)
-let h_fix ido n      = abstract_tactic (TacFix (ido,n)) (fix ido n)
-let h_mutual_fix b id n l =
-  abstract_tactic
-    (TacMutualFix (b,id,n,l))
-    (mutual_fix id n l 0)
+let h_apply_in simple ev cb (id,ipat) =
+  abstract_tactic (apply_in simple ev id cb ipat)
+let h_elim ev cb cbo    = abstract_tactic (elim ev cb cbo)
+let h_elim_type c    = abstract_tactic (elim_type c)
+let h_case ev cb     = abstract_tactic (general_case_analysis ev cb)
+let h_case_type c    = abstract_tactic (case_type c)
+let h_fix ido n      = abstract_tactic (fix ido n)
+let h_mutual_fix b id n l = abstract_tactic (mutual_fix id n l 0)
 
-let h_cofix ido      = abstract_tactic (TacCofix ido) (cofix ido)
-let h_mutual_cofix b id l =
-  abstract_tactic
-    (TacMutualCofix (b,id,l))
-    (mutual_cofix id l 0)
+let h_cofix ido      = abstract_tactic (cofix ido)
+let h_mutual_cofix b id l = abstract_tactic (mutual_cofix id l 0)
 
-let h_cut c          = abstract_tactic (TacCut c) (cut c)
+let h_cut c          = abstract_tactic (cut c)
 let h_generalize_gen cl =
-  abstract_tactic (TacGeneralize cl)
+  abstract_tactic
     (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
 let h_generalize cl =
   h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
     cl)
 let h_generalize_dep c =
-  abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
+  abstract_tactic (generalize_dep c)
 let h_let_tac b na c cl eqpat =
   let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
   let with_eq = if b then None else Some (true,id) in
-  abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
-    (letin_tac with_eq na c None cl)
+  abstract_tactic (letin_tac with_eq na c None cl)
 let h_let_pat_tac b na c cl eqpat =
   let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
   let with_eq = if b then None else Some (true,id) in
-  abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
-    (letin_pat_tac with_eq na c None cl)
+  abstract_tactic (letin_pat_tac with_eq na c None cl)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
-  abstract_tactic (TacSimpleInductionDestruct (isrec,h))
-    (if isrec then (simple_induct h) else (simple_destruct h))
+  abstract_tactic (if isrec then (simple_induct h) else (simple_destruct h))
 let h_simple_induction = h_simple_induction_destruct true
 let h_simple_destruct = h_simple_induction_destruct false
 
-let out_indarg = function
-  | ElimOnConstr (_,c) -> ElimOnConstr c
-  | ElimOnIdent id -> ElimOnIdent id
-  | ElimOnAnonHyp n -> ElimOnAnonHyp n
-
 let h_induction_destruct isrec ev lcl =
-  let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
-  abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
-    (induction_destruct isrec ev lcl)
+  abstract_tactic (induction_destruct isrec ev lcl)
 let h_new_induction ev c idl e cl =
   h_induction_destruct true ev ([c,idl],e,cl)
 let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
 
-let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
-let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
+let h_specialize n d = abstract_tactic (specialize n d)
+let h_lapply c = abstract_tactic (cut_and_apply c)
 
 (* Context management *)
-let h_clear b l = abstract_tactic (TacClear (b,l))
-  ((if b then keep else clear) l)
-let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
-let h_move dep id1 id2 =
-  abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
-let h_rename l =
-  abstract_tactic (TacRename l) (rename_hyp l)
-let h_revert l = abstract_tactic (TacRevert l) (revert l)
+let h_clear b l = abstract_tactic ((if b then keep else clear) l)
+let h_clear_body l = abstract_tactic (clear_body l)
+let h_move dep id1 id2 = abstract_tactic (move_hyp dep id1 id2)
+let h_rename l = abstract_tactic (rename_hyp l)
+let h_revert l = abstract_tactic (revert l)
 
 (* Constructors *)
-let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l)
-let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l)
-let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l)
+let h_left ev l  = abstract_tactic (left_with_bindings ev l)
+let h_right ev l = abstract_tactic (right_with_bindings ev l)
+let h_split ev l = abstract_tactic (split_with_bindings ev l)
 (* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
   abstract_tactic (TacAnyConstructor t) (any_constructor t)
 *)
 let h_constructor ev n l =
-  abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l)
+  abstract_tactic (constructor_tac ev None n l)
 let h_one_constructor n =
-  abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings)
+  abstract_tactic (one_constructor n NoBindings)
 let h_simplest_left   = h_left false NoBindings
 let h_simplest_right  = h_right false NoBindings
 
 (* Conversion *)
 let h_reduce r cl  =
-  abstract_tactic (TacReduce (r,cl)) (reduce r cl)
+  abstract_tactic (reduce r cl)
 let h_change op c cl =
-  abstract_tactic (TacChange (op,c,cl)) (change op c cl)
+  abstract_tactic (change op c cl)
 
 (* Equivalence relations *)
-let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
-let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
-let h_transitivity c =
-  abstract_tactic (TacTransitivity c)
-    (intros_transitivity c)
+let h_reflexivity    = abstract_tactic intros_reflexivity
+let h_symmetry c     = abstract_tactic (intros_symmetry c)
+let h_transitivity c = abstract_tactic (intros_transitivity c)
 
 let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)]
 let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)]
 let h_simplest_elim c   = h_elim false (c,NoBindings) None
 let h_simplest_case   c = h_case false (c,NoBindings)
 
-let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
+let h_intro_patterns l = abstract_tactic (intro_patterns l)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 12c970d68e..2ed054ea18 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2380,7 +2380,7 @@ and interp_atomic ist gl tac =
       let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in
       tclTHEN
 	(tclEVARS sigma)
-	(abstract_tactic (TacAssert (t,ipat,c))
+	(abstract_tactic
            (Tactics.forward (Option.map (interp_tactic ist) t)
 	      (Option.map (interp_intro_pattern ist gl) ipat) c))
   | TacGeneralize cl ->
@@ -2479,7 +2479,7 @@ and interp_atomic ist gl tac =
       let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
       tclWITHHOLES ev (h_split ev) sigma bll
   | TacAnyConstructor (ev,t) ->
-      abstract_tactic (TacAnyConstructor (ev,t))
+      abstract_tactic
         (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
   | TacConstructor (ev,n,bl) ->
       let sigma, bl = interp_bindings ist env sigma bl in
@@ -2569,7 +2569,7 @@ and interp_atomic ist gl tac =
 	  sigma , a_interp::acc
 	end l (project gl,[])
       in
-      abstract_extended_tactic opn args (tac args)
+      abstract_extended_tactic (tac args)
   | TacAlias (loc,s,l,(_,body)) -> fun gl ->
     let evdref = ref gl.sigma in
     let f x = match genarg_tag x with
@@ -2706,16 +2706,15 @@ let eval_ltac_constr gl t =
     { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl
     (intern_tactic_or_tacarg (make_empty_glob_sign ()) t )
 
-(* Hides interpretation for pretty-print *)
+(* Used to hide interpretation for pretty-print, now just launch tactics *)
 let hide_interp t ot gl =
   let ist = { ltacvars = ([],[]); ltacrecvars = [];
             gsigma = project gl; genv = pf_env gl } in
   let te = intern_tactic true ist t in
   let t = eval_tactic te in
   match ot with
-  | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl
-  | Some t' ->
-      abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl
+  | None -> abstract_tactic_expr t gl
+  | Some t' -> abstract_tactic_expr (tclTHEN t t') gl
 
 (***************************************************************************)
 (* Substitution at module closing time *)