Removing some tactic compatibility layer.

5 files changed, 28 insertions, 17 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index faeb9fc25..805ecc3eb 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,7 @@ let absurd c gls =
   let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
   let c = j.Environ.utj_val in
   (tclTHENS
-     (tclTHEN (elim_type (build_coq_False ())) (Proofview.V82.of_tactic (cut c)))
+     (tclTHEN (Proofview.V82.of_tactic (elim_type (build_coq_False ()))) (Proofview.V82.of_tactic (cut c)))
      ([(tclTHENS
           (Proofview.V82.of_tactic (cut (mkApp(build_coq_not (),[|c|]))))
 	  ([(tclTHEN (Proofview.V82.of_tactic intros)
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 02dded782..a07069bd3 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -39,11 +39,11 @@ TACTIC EXTEND vm_cast_no_check
 END
 
 TACTIC EXTEND casetype
-  [ "casetype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.case_type c) ]
+  [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
 END
 
 TACTIC EXTEND elimtype
-  [ "elimtype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.elim_type c) ]
+  [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
 END
 
 TACTIC EXTEND lapply
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c18fd31d0..5aceeb9f4 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -138,7 +138,7 @@ let solveArg eqonleft op a1 a2 tac =
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
     else [diseqCase eqonleft;eqCase tac;default_auto] in
-  (tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs)
+  (tclTHENS (elim_type decide) subtacs)
   end
 
 let solveEqBranch rectype =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18c558532..f1cb06c4e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -903,6 +903,11 @@ let find_ind_eliminator ind s gl =
   let evd, c = pf_apply Evd.fresh_global gl gr in
     evd, c
 
+let new_find_ind_eliminator ind s gl =
+  let gr = lookup_eliminator ind s in
+  let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in
+    evd, c
+
 let find_eliminator c gl =
   let ((ind,u),t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   if is_record ind <> None then raise IsRecord;
@@ -3481,28 +3486,34 @@ let simple_destruct = function
  * May be they should be integrated into Elim ...
  *)
 
-let elim_scheme_type elim t gl =
-  let clause = mk_clenv_type_of gl elim in
+let elim_scheme_type elim t =
+  Proofview.Goal.enter begin fun gl ->
+  let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
   match kind_of_term (last_arg clause.templval.rebus) with
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
-	Proofview.V82.of_tactic (Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false) gl
+	Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
     | _ -> anomaly (Pp.str "elim_scheme_type")
+  end
 
-let elim_type t gl =
-  let (ind,t) = pf_reduce_to_atomic_ind gl t in
-  let evd, elimc = find_ind_eliminator (fst ind) (elimination_sort_of_goal gl) gl in
-    tclTHEN (tclEVARS evd) (elim_scheme_type elimc t) gl
+let elim_type t =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
+  let evd, elimc = new_find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
+  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t)
+  end
 
-let case_type t gl =
-  let (ind,t) = pf_reduce_to_atomic_ind gl t in
+let case_type t =
+  Proofview.Goal.raw_enter begin fun gl ->
+  let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc =
-    pf_apply build_case_analysis_scheme_default gl ind (elimination_sort_of_goal gl)
+    Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl)
   in
-    tclTHEN (tclEVARS evd) (elim_scheme_type elimc t) gl
+  Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t)
+  end
 
 
 (************************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5951a4af8..7d88b7a90 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -286,8 +286,8 @@ val induction_destruct : rec_flag -> evars_flag ->
 
 (** {6 Eliminations giving the type instead of the proof. } *)
 
-val case_type         : constr  -> tactic
-val elim_type         : constr  -> tactic
+val case_type         : constr  -> unit Proofview.tactic
+val elim_type         : constr  -> unit Proofview.tactic
 
 (** {6 Introduction tactics. } *)