Moving some tactic code to the new engine.

12 files changed, 159 insertions, 138 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 966d247e0..444043dbe 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -496,8 +496,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
 let make_clenv_binding_env_apply env sigma n =
   make_clenv_binding_gen true n env sigma
 	
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
-let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
+let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
+let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7731c4ca2..9a985a842 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -100,10 +100,10 @@ val make_clenv_binding_env_apply :
    clausenv
 
 val make_clenv_binding_apply :
-  Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
-  Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> constr * constr -> constr bindings -> clausenv
 
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a9146a96a..943974489 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -221,6 +221,7 @@ module New = struct
   let pf_type_of gl t =
     pf_apply type_of gl t
 
+  let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
   let pf_ids_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
@@ -253,11 +254,21 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl gl =
+  let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Proofview.Goal.sigma gl in
     nf_evar sigma concl
 
+  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+
+  let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
+
+  let pf_reduce_to_quantified_ind gl t =
+    pf_apply reduce_to_quantified_ind gl t
+
+  let pf_hnf_type_of gl t =
+    pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9a53560b6..bf0ce04a1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,15 +134,19 @@ module New : sig
   val pf_global : identifier -> 'a Proofview.Goal.t -> constr
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
-  val pf_type_of : 'b Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'b Proofview.Goal.t -> identifier list
-  val pf_hyps_types : 'b Proofview.Goal.t -> (identifier * types) list
+  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
 
   val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
   val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
   val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types
+  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
 end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a0a5dddb8..b16f956d0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,7 +134,7 @@ let side_tac tac sidetac =
   | Some sidetac -> Tacticals.New.tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac
 
 let instantiate_lemma_all frzevars env gl c ty l l2r concl =
-  let eqclause = Clenv.make_clenv_binding gl (c,ty) l in
+  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
   let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
   let rec split_last_two = function
       | [c1;c2] -> [],(c1, c2)
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars env gl c ty l l2r concl =
 let instantiate_lemma env gl c ty l l2r concl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let eqclause = Clenv.make_clenv_binding gl (c,t) l in
+  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
 
 let rewrite_conv_closed_unif_flags = {
@@ -880,13 +880,11 @@ let onEquality with_evars tac (c,lbindc) =
   try (* type_of can raise exceptions *)
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
-  let eq_clause = Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) gl in
+  let eq_clause = Tacmach.New.pf_apply make_clenv_binding gl (c,t') lbindc in
   begin try (* clenv_pose_dependent_evars can raise exceptions *)
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let (eq,eq_args) =
-    Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) gl
-  in
+  let (eq,eq_args) = find_this_eq_data_decompose gl eqn in
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
     (tac (eq,eqn,eq_args) eq_clause')
@@ -1319,7 +1317,7 @@ let swap_equality_args = function
   | PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1]
   | HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1]
 
-let swap_equands gls eqn =
+let swap_equands eqn =
   let (lbeq,eq_args) = find_eq_data eqn in
   applist(lbeq.eq,swap_equality_args eq_args)
 
@@ -1416,69 +1414,80 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 
 exception NothingToRewrite
 
-let cutSubstInConcl_RL eqn gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
-  let body,expected_goal = pf_apply subst_tuple_term gls e2 e1 (pf_concl gls) in
+let cutSubstInConcl_RL eqn =
+  Proofview.Goal.enter begin fun gl ->
+  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
+  let concl = Proofview.Goal.concl gl in
+  let body,expected_goal = Tacmach.New.pf_apply subst_tuple_term gl e2 e1 concl in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  tclTHENFIRST
+  Proofview.V82.tactic (fun gl -> tclTHENFIRST
     (bareRevSubstInConcl lbeq body eq)
-    (convert_concl expected_goal DEFAULTcast) gls
+    (convert_concl expected_goal DEFAULTcast) gl)
+  end
 
 (* |- (P e1)
      BY CutSubstInConcl_LR (eq T e1 e2)
      |- (P e2)
      |- (eq T e1 e2)
  *)
-let cutSubstInConcl_LR eqn gls =
-  (tclTHENS (cutSubstInConcl_RL (swap_equands gls eqn))
+let cutSubstInConcl_LR eqn =
+  Proofview.V82.tactic (fun gl ->
+  (tclTHENS (Proofview.V82.of_tactic (cutSubstInConcl_RL (swap_equands eqn)))
      ([tclIDTAC;
-       swapEquandsInConcl])) gls
+       swapEquandsInConcl])) gl)
 
 let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
 
-let cutSubstInHyp_LR eqn id gls =
-  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
-  let idtyp = pf_get_hyp_typ gls id in
-  let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in
+let cutSubstInHyp_LR eqn id =
+  Proofview.Goal.enter begin fun gl ->
+  let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
+  let idtyp = Tacmach.New.pf_get_hyp_typ id gl in
+  let body,expected_goal = Tacmach.New.pf_apply subst_tuple_term gl e1 e2 idtyp in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  cut_replacing id expected_goal
+  Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal
     (tclTHENFIRST
       (bareRevSubstInConcl lbeq body eq)
-      (refine_no_check (mkVar id))) gls
+      (refine_no_check (mkVar id))) gl)
+  end
 
-let cutSubstInHyp_RL eqn id gls =
-  (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id)
+let cutSubstInHyp_RL eqn id =
+  Proofview.V82.tactic (fun gl ->
+  (tclTHENS (Proofview.V82.of_tactic (cutSubstInHyp_LR (swap_equands eqn) id))
      ([tclIDTAC;
-       swapEquandsInConcl])) gls
+       swapEquandsInConcl])) gl)
 
 let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL
 
-let try_rewrite tac gls =
-  try
-    tac gls
-  with
+let try_rewrite tac =
+  Proofview.tclORELSE tac begin function
     | ConstrMatching.PatternMatchingFailure ->
-	errorlabstrm "try_rewrite" (str "Not a primitive equality here.")
+	Tactics.New.tclZEROMSG (str "Not a primitive equality here.")
     | e when catchable_exception e ->
-	errorlabstrm "try_rewrite"
+	Tactics.New.tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
     | NothingToRewrite ->
-	errorlabstrm "try_rewrite"
+	Tactics.New.tclZEROMSG
           (strbrk "Nothing to rewrite.")
+    | e -> Proofview.tclZERO e
+  end
 
-let cutSubstClause l2r eqn cls gls =
+let cutSubstClause l2r eqn cls =
   match cls with
-    | None ->    cutSubstInConcl l2r eqn gls
-    | Some id -> cutSubstInHyp l2r eqn id gls
+    | None ->    cutSubstInConcl l2r eqn
+    | Some id -> cutSubstInHyp l2r eqn id
 
 let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls)
 let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
-let substClause l2r c cls gls =
-  let eq = pf_apply get_type_of gls c in
+let substClause l2r c cls =
+  let open Tacmach.New in
+  let open Tacticals.New in
+  Proofview.Goal.raw_enter begin fun gl ->
+  let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
-    [tclIDTAC; exact_no_check c] gls
+    [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
+  end
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1591,7 +1600,7 @@ let subst_one_var dep_proof_ok x =
       (* x is a variable: *)
       let varx = mkVar x in
       (* Find a non-recursive definition for x *)
-      let found gl =
+      let res =
         try
           let test hyp _ = is_eq_x gl varx hyp in
           Context.fold_named_context test ~init:() hyps;
@@ -1599,8 +1608,7 @@ let subst_one_var dep_proof_ok x =
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
         with FoundHyp res -> res in
-      let (hyp,rhs,dir) = Tacmach.New.of_old found gl in
-      subst_one dep_proof_ok x (hyp,rhs,dir)
+      subst_one dep_proof_ok x res
   end
 
 let subst_gen dep_proof_ok ids =
@@ -1625,7 +1633,7 @@ let default_subst_tactic_flags () =
 
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
   Proofview.Goal.enter begin fun gl ->
-  let find_eq_data_decompose = Tacmach.New.of_old find_eq_data_decompose gl in
+  let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
     try
       let lbeq,(_,x,y) = find_eq_data_decompose c in
@@ -1649,27 +1657,23 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = snd (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true else failwith "not convertible"
+    if Tacmach.New.pf_conv_x gl c x then true else failwith "not convertible"
   with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
     let (_,_,x) = snd (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then false else failwith "not convertible"
+    if Tacmach.New.pf_conv_x gl c x then false else failwith "not convertible"
   with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
     let (_,x,y) = snd (find_eq_data_decompose gl t) in
-    if pf_conv_x gl c x then true
-    else if pf_conv_x gl c y then false
+    if Tacmach.New.pf_conv_x gl c x then true
+    else if Tacmach.New.pf_conv_x gl c y then false
     else failwith "not convertible"
   with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
 
-let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t)
-let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
-let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t)
-
 let rewrite_multi_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
     | [] -> error "No such assumption."
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 681b366db..d5aa2d248 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -94,15 +94,15 @@ val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
 
 (* The family cutRewriteIn expect an equality statement *)
-val cutRewriteInHyp : bool -> types -> Id.t -> tactic
-val cutRewriteInConcl : bool -> constr -> tactic
+val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic
+val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 
 (* The family rewriteIn expect the proof of an equality *)
-val rewriteInHyp : bool -> constr -> Id.t -> tactic
-val rewriteInConcl : bool -> constr -> tactic
+val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
+val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
 (* Expect the proof of an equality; fails with raw internal errors *)
-val substClause : bool -> constr -> Id.t option -> tactic
+val substClause : bool -> constr -> Id.t option -> unit Proofview.tactic
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
 val injectable : env -> evar_map -> constr -> constr -> bool
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a397976ea..9ed937447 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -165,15 +165,15 @@ let injHyp id =
   injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
 
 TACTIC EXTEND dependent_rewrite
-| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ Proofview.V82.tactic (rewriteInConcl b c) ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
 | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
-    -> [ Proofview.V82.tactic (rewriteInHyp b c id) ]
+    -> [ rewriteInHyp b c id ]
 END
 
 TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ Proofview.V82.tactic (cutRewriteInConcl b eqn) ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
 | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
-    -> [ Proofview.V82.tactic (cutRewriteInHyp b eqn id) ]
+    -> [ cutRewriteInHyp b eqn id ]
 END
 
 (**********************************************************************)
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 80720cfaf..cc3c4c297 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -396,10 +396,10 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = Tacmach.pf_type_of gl e1 in (t,e1,e2)
+      let t = Tacmach.New.pf_type_of gl e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if Tacmach.pf_conv_x gl t1 t2 then (t1,e1,e2)
+      if Tacmach.New.pf_conv_x gl t1 t2 then (t1,e1,e2)
       else raise PatternMatchingFailure
 
 let find_eq_data_decompose gl eqn =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 4735b26b3..f8a4d35a8 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -120,11 +120,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : Proof_type.goal sigma -> constr ->
+val find_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
       coq_eq_data * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proof_type.goal sigma -> constr ->
+val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
       coq_eq_data * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 06853e137..d2dd64e52 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -300,7 +300,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
 
 let projectAndApply thin id eqname names depids =
   let subst_hyp l2r id =
-    tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
+    tclTHEN (tclTRY(Proofview.V82.of_tactic (rewriteInConcl l2r (mkVar id))))
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 718c039fa..c61192031 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -695,10 +695,10 @@ let resolve_classes gl =
 (**************************)
 
 let cut c =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let concl = Proofview.Goal.concl gl in
+    let concl = Tacmach.New.pf_nf_concl gl in
     let is_sort =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
@@ -836,13 +836,13 @@ let general_elim_clause_gen elimtac indclause elim gl =
   let elimt = pf_type_of gl elimc in
   let i =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
-  let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
+  let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
   elimtac i elimclause indclause gl
 
 let general_elim_clause elimtac (c,lbindc) elim gl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let indclause  = make_clenv_binding gl (c,t) lbindc  in
+  let indclause  = pf_apply make_clenv_binding gl (c,t) lbindc  in
     general_elim_clause_gen elimtac indclause elim gl
 
 let general_elim with_evars c e =
@@ -1035,7 +1035,7 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
     let try_apply thm_ty nprod =
       let n = nb_prod thm_ty - nprod in
 	if n<0 then error "Applied theorem has not enough premisses.";
-	let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+	let clause = pf_apply make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
 	Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl
     in
       try try_apply thm_ty0 concl_nprod
@@ -1116,7 +1116,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise e
   in
-  aux (make_clenv_binding gl (d,thm) lbind)
+  aux (pf_apply make_clenv_binding gl (d,thm) lbind)
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars id
   (loc,(d,lbind)) gl0 =
@@ -1225,13 +1225,13 @@ let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
 let clear_body = thin_body
 
 let clear_wildcards ids =
-  tclMAP (fun (loc,id) gl ->
+  Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
     try with_check (Tacmach.thin_no_check [id]) gl
     with ClearDependencyError (id,err) ->
       (* Intercept standard [thin] error message *)
       Loc.raise loc
         (error_clear_dependency (pf_env gl) (Id.of_string "_") err))
-    ids
+    ids)
 
 (*   Takes a list of booleans, and introduces all the variables
  *  quantified in the goal which are associated with a value
@@ -1252,7 +1252,7 @@ let specialize mopt (c,lbind) g =
       let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
 	tclEVARS evd, nf_evar evd c
     else
-      let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+      let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in
       let flags = { default_unify_flags with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
@@ -1314,8 +1314,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if i > nconstr then error "Not enough constructors."
 
 let constructor_tac with_evars expctdnumopt i lbind =
-  Proofview.Goal.enter begin fun gl ->
-    let cl = Proofview.Goal.concl gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+    let cl = Tacmach.New.pf_nf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
@@ -1346,8 +1346,8 @@ let rec tclANY tac = function
 let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
   let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
-  Proofview.Goal.enter begin fun gl ->
-    let cl = Proofview.Goal.concl gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+    let cl = Tacmach.New.pf_nf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
@@ -1414,22 +1414,23 @@ let my_find_eq_data_decompose gl t =
        known equalities will be dynamically registered *)
       -> raise ConstrMatching.PatternMatchingFailure
 
-let intro_decomp_eq loc b l l' thin tac id gl =
+let intro_decomp_eq loc b l l' thin tac id =
+  Proofview.Goal.raw_enter begin fun gl ->
   let c = mkVar id in
-  let _,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  let t = Tacmach.New.pf_type_of gl c in
+  let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let eq,eq_args = my_find_eq_data_decompose gl t in
-  let eq_clause = make_clenv_binding gl (c,t) NoBindings in
-  Proofview.V82.of_tactic (!intro_decomp_eq_function
+  let eq_clause = Tacmach.New.pf_apply make_clenv_binding gl (c,t) NoBindings in
+  !intro_decomp_eq_function
     (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
-    (eq,t,eq_args) eq_clause) gl
+    (eq,t,eq_args) eq_clause
+  end
 
 let intro_or_and_pattern loc b ll l' thin tac id =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   let c = mkVar id in
-  let (ind,t) =
-    Tacmach.New.of_old (fun gl ->
-      pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
-  in
+  let t = Tacmach.New.pf_type_of gl c in
+  let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
   let nv = mis_constr_nargs ind in
   let bracketed = b || not (List.is_empty l') in
   let adjust n l = if bracketed then adjust_intro_patterns n l else l in
@@ -1448,7 +1449,7 @@ let rewrite_hyp l2r id =
     Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_type_of gl in
     let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
@@ -1533,8 +1534,8 @@ let rec intros_patterns b avoid ids thin destopt tac = function
 	   (fun thin -> intros_patterns b avoid ids thin destopt tac))
   | (loc, IntroInjection l) :: l' ->
       intro_then_force (fun id ->
-	(Proofview.V82.tactic (intro_decomp_eq loc b l l' thin
-	   (fun thin -> intros_patterns b avoid ids thin destopt tac) id)))
+        intro_decomp_eq loc b l l' thin
+          (fun thin -> intros_patterns b avoid ids thin destopt tac) id)
   | (loc, IntroRewrite l2r) :: l ->
       intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
 	MoveLast true false
@@ -1545,7 +1546,7 @@ let rec intros_patterns b avoid ids thin destopt tac = function
   | [] -> tac ids thin
 
 let intros_pattern destopt =
-  intros_patterns false [] [] [] destopt (fun _ l -> Proofview.V82.tactic (clear_wildcards l))
+  intros_patterns false [] [] [] destopt (fun _ l -> clear_wildcards l)
 
 let intro_pattern destopt pat =
   intros_pattern destopt [dloc,pat]
@@ -1558,11 +1559,11 @@ let intro_patterns = function
 (*   Other cut tactics    *)
 (**************************)
 
-let make_id s = fresh_id [] (default_id_of_sort s)
+let make_id s = new_fresh_id [] (default_id_of_sort s)
 
 let prepare_intros s ipat gl =
-  let make_id s = Tacmach.New.of_old (make_id s) gl in
-  let fresh_id l id = Tacmach.New.of_old (fresh_id l id) gl in
+  let make_id s = make_id s gl in
+  let fresh_id l id = new_fresh_id l id gl in
   match ipat with
   | None ->
       make_id s , Proofview.tclUNIT ()
@@ -1575,7 +1576,7 @@ let prepare_intros s ipat gl =
       fresh_id [] id , Proofview.tclUNIT ()
   | IntroWildcard ->
       let id = make_id s in
-      id , Proofview.V82.tactic (clear_wildcards [dloc,id])
+      id , clear_wildcards [dloc,id]
   | IntroRewrite l2r ->
       let id = make_id s in
       id , Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
@@ -1583,13 +1584,12 @@ let prepare_intros s ipat gl =
       make_id s ,
       Tacticals.New.onLastHypId
 	(intro_or_and_pattern loc true ll [] []
-	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
+	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l)))
   | IntroInjection l ->
       make_id s ,
-      Proofview.V82.tactic (onLastHypId
+      Tacticals.New.onLastHypId
 	(intro_decomp_eq loc true l [] []
-	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
-      )
+	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l)))
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected")
 
@@ -1610,8 +1610,8 @@ let clear_if_overwritten c ipats =
   | _ -> tclIDTAC
 
 let assert_as first ipat c =
-  Proofview.Goal.enter begin fun gl ->
-  let hnf_type_of = Tacmach.New.of_old pf_hnf_type_of gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+  let hnf_type_of = Tacmach.New.pf_hnf_type_of gl in
   match kind_of_term (hnf_type_of c) with
   | Sort s ->
       let (id,tac) = prepare_intros s ipat gl in
@@ -1631,12 +1631,12 @@ let as_tac id ipat = match ipat with
       Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll [] []
-        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l)))
+        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l))
         id
   | Some (loc,IntroInjection l) ->
-      Proofview.V82.tactic (intro_decomp_eq loc true l [] []
-        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l)))
-        id)
+      intro_decomp_eq loc true l [] []
+        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l))
+        id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
        IntroWildcard | IntroForthcoming _)) ->
@@ -1955,8 +1955,8 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
     let (newcl,eq_tac) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
-            | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) gl
-	    | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) gl
+            | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
+	    | IntroFresh heq_base -> new_fresh_id [id] heq_base gl
             | IntroIdentifier id -> id
 	    | _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in
             let eqdata = build_coq_eq_data () in
@@ -1983,7 +1983,7 @@ let letin_tac with_eq name c ty occs =
   letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
 
 let letin_pat_tac with_eq name c ty occs =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
   letin_tac_gen with_eq name c
@@ -1995,7 +1995,7 @@ let letin_pat_tac with_eq name c ty occs =
 let forward usetac ipat c =
   match usetac with
   | None ->
-      Proofview.Goal.enter begin fun gl ->
+      Proofview.Goal.raw_enter begin fun gl ->
       let type_of = Tacmach.New.pf_type_of gl in
       begin try (* type_of can raise an exception *)
               let t = type_of c in
@@ -2084,18 +2084,18 @@ let check_unused_names names =
        ++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names)
 
 let rec consume_pattern avoid id isdep gl = function
-  | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
+  | [] -> ((dloc, IntroIdentifier (new_fresh_id avoid id gl)), [])
   | (loc,IntroAnonymous)::names ->
       let avoid = avoid@explicit_intro_names names in
-      ((loc,IntroIdentifier (fresh_id avoid id gl)), names)
+      ((loc,IntroIdentifier (new_fresh_id avoid id gl)), names)
   | (loc,IntroForthcoming true)::names when not isdep ->
       consume_pattern avoid id isdep gl names
   | (loc,IntroForthcoming _)::names as fullpat ->
       let avoid = avoid@explicit_intro_names names in
-      ((loc,IntroIdentifier (fresh_id avoid id gl)), fullpat)
+      ((loc,IntroIdentifier (new_fresh_id avoid id gl)), fullpat)
   | (loc,IntroFresh id')::names ->
       let avoid = avoid@explicit_intro_names names in
-      ((loc,IntroIdentifier (fresh_id avoid id' gl)), names)
+      ((loc,IntroIdentifier (new_fresh_id avoid id' gl)), names)
   | pat::names -> (pat,names)
 
 let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
@@ -2154,32 +2154,32 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
     match ra with
     | (RecArg,deprec,recvarname) ::
         (IndArg,depind,hyprecname) :: ra' ->
-        Proofview.Goal.enter begin fun gl ->
+        Proofview.Goal.raw_enter begin fun gl ->
         let (recpat,names) = match names with
           | [loc,IntroIdentifier id as pat] ->
               let id' = next_ident_away (add_prefix "IH" id) avoid in
 	      (pat, [dloc, IntroIdentifier id'])
-          | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) gl in
+          | _ -> consume_pattern avoid recvarname deprec gl names in
         let dest = get_recarg_dest dests in
         safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
-        Proofview.Goal.enter begin fun gl ->
+        Proofview.Goal.raw_enter begin fun gl ->
           let (hyprec,names) =
-            Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) gl
+            consume_pattern avoid hyprecname depind gl names
           in
 	  safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
 	    peel_tac ra' (update_dest dests ids') names thin)
         end)
         end
     | (IndArg,dep,hyprecname) :: ra' ->
-        Proofview.Goal.enter begin fun gl ->
+        Proofview.Goal.raw_enter begin fun gl ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
-        let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) gl in
+        let (pat,names) = consume_pattern avoid hyprecname dep gl names in
 	safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
         end
     | (RecArg,dep,recvarname) :: ra' ->
-        Proofview.Goal.enter begin fun gl ->
-        let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) gl in
+        Proofview.Goal.raw_enter begin fun gl ->
+        let (pat,names) = consume_pattern avoid recvarname dep gl names in
         let dest = get_recarg_dest dests in
 	safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
@@ -2193,7 +2193,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
         peel_tac ra' dests names thin)
     | [] ->
         check_unused_names names;
-        Tacticals.New.tclTHEN (Proofview.V82.tactic (clear_wildcards thin)) (tac dests)
+        Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
   in
   peel_tac ra dests names []
 
@@ -2230,7 +2230,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 	| Var id when not (List.exists (occur_var env id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid)
 	| Var id ->
-            let x = Tacmach.New.of_old (fresh_id [] id) gl in
+            let x = new_fresh_id [] id gl in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
@@ -2238,7 +2238,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
             let type_of = Tacmach.New.pf_type_of gl in
 	    let id = id_of_name_using_hdchar (Global.env()) (type_of c)
 		       Anonymous in
-            let x = Tacmach.New.of_old (fresh_id [] id) gl in
+            let x = new_fresh_id [] id gl in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
@@ -3102,7 +3102,7 @@ let get_eliminator elim gl = match elim with
   | ElimUsing (elim,indsign) ->
       (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
-      let (elimc,elimt),_ as elims = guess_elim isrec id gl in
+      let (elimc,elimt),_ as elims = Tacmach.New.of_old (guess_elim isrec id) gl in
       isrec, ({elimindex = None; elimbody = elimc}, elimt),
       fst (compute_elim_signature elims id)
 
@@ -3153,7 +3153,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
   let {elimbody=(elimc,lbindelimc)},elimt = elim in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimclause =
-    make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
+    pf_apply make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv nparams indvars elimclause gl in
   (* one last resolution (useless?) *)
@@ -3165,7 +3165,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
 
 let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names tac =
   Proofview.Goal.enter begin fun gl ->
-  let (isrec, elim, indsign) = Tacmach.New.of_old (get_eliminator elim) gl in
+  let (isrec, elim, indsign) = get_eliminator elim gl in
   let names = compute_induction_names (Array.length indsign) names in
   (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
     (Tacticals.New.tclTHEN
@@ -3252,10 +3252,10 @@ let induction_from_context_l with_evars elim_info lid names =
    hypothesis on which the induction is made *)
 let induction_tac with_evars elim (varname,lbind) typ gl =
   let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in
-  let indclause = make_clenv_binding gl (mkVar varname,typ) lbind  in
+  let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind  in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   let elimclause =
-    make_clenv_binding gl
+    pf_apply make_clenv_binding gl
       (mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in
   elimination_clause_scheme with_evars i elimclause indclause gl
 
@@ -3615,9 +3615,8 @@ let dImp cls =
 let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let maybe_betadeltaiota_concl allowred gl =
-  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+  let concl = Tacmach.New.pf_nf_concl gl in
   let sigma = Proofview.Goal.sigma gl in
-  let concl = nf_evar sigma concl in
   if not allowred then concl
   else
     let env = Proofview.Goal.env gl in
@@ -3928,4 +3927,6 @@ module New = struct
       )
     end
 
+  let tclZEROMSG = tclZEROMSG
+
 end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9f4f0e9ce..f3c5e7d26 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -417,4 +417,5 @@ module New : sig
 
   open Proofview
   val exact_proof : Constrexpr.constr_expr -> unit tactic
+  val tclZEROMSG : Pp.std_ppcmds -> unit tactic
 end