Putting all the tactics exported by the Tactics module in the new monad API.

31 files changed, 428 insertions, 451 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 8b5f527cd..ce28eacc0 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,15 +39,15 @@ TACTIC EXTEND cut
 END
 
 TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
 END
 
 TACTIC EXTEND vm_cast_no_check
-  [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ]
+  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
 END
 
 TACTIC EXTEND native_cast_no_check
-  [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ]
+  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
 END
 
 TACTIC EXTEND casetype
@@ -200,10 +200,10 @@ END
 (** Move *)
 
 TACTIC EXTEND move
-  [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ]
+  [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
+| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
+| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
+| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
 (** Revert *)
@@ -231,15 +231,15 @@ END
 (* Fix *)
 
 TACTIC EXTEND fix
-  [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
-| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+  [ "fix" natural(n) ] -> [ Tactics.fix None n ]
+| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
 END
 
 (* Cofix *)
 
 TACTIC EXTEND cofix
-  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
-| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+  [ "cofix" ] -> [ Tactics.cofix None ]
+| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
 END
 
 (* Clear *)
@@ -247,7 +247,7 @@ END
 TACTIC EXTEND clear
   [ "clear" hyp_list(ids) ] -> [
     if List.is_empty ids then Tactics.keep []
-    else Proofview.V82.tactic (Tactics.clear ids)
+    else Tactics.clear ids
   ]
 | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
 END
@@ -261,7 +261,7 @@ END
 (* Generalize dependent *)
 
 TACTIC EXTEND generalize_dependent
-  [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ]
+  [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
 END
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 1f3eb1335..451e0987b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -582,7 +582,7 @@ END
     during dependent induction. For internal use. *)
 
 TACTIC EXTEND specialize_eqs
-[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ]
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
 END
 
 (**********************************************************************)
@@ -728,7 +728,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
        Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+         [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d650cb5c6..5d282a693 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma)
+        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
       end }
       end
   | TacApply (a,ev,cb,cl) ->
@@ -1714,7 +1714,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) in
+        let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
@@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in
+        let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+          (Tactics.generalize_gen cl)) sigma
       end }
   | TacLetTac (na,c,clp,b,eqpat) ->
       Proofview.V82.nf_evar_goals <*>
@@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           in
           Sigma.Unsafe.of_pair (c, sigma)
         end } in
-        Proofview.V82.tactic (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl))
+        Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
       end }
       end
   | TacChange (Some op,c,cl) ->
@@ -1889,25 +1889,22 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
-        Proofview.V82.tactic begin fun gl -> 
-          let op = interp_typed_pattern ist env sigma op in
-          let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-          let c_interp patvars = { Sigma.run = begin fun sigma ->
-	    let lfun' = Id.Map.fold (fun id c lfun ->
-	      Id.Map.add id (Value.of_constr c) lfun) 
-	      patvars ist.lfun
-	    in
-	    let ist = { ist with lfun = lfun' } in
-	      try
-                let sigma = Sigma.to_evar_map sigma in
-                let (sigma, c) = interp_constr ist env sigma c in
-                Sigma.Unsafe.of_pair (c, sigma)
-	      with e when to_catch e (* Hack *) ->
-		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
-          end } in
-	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-	      gl
-        end
+        let op = interp_typed_pattern ist env sigma op in
+        let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+        let c_interp patvars = { Sigma.run = begin fun sigma ->
+          let lfun' = Id.Map.fold (fun id c lfun ->
+            Id.Map.add id (Value.of_constr c) lfun) 
+            patvars ist.lfun
+          in
+          let ist = { ist with lfun = lfun' } in
+            try
+              let sigma = Sigma.to_evar_map sigma in
+              let (sigma, c) = interp_constr ist env sigma c in
+              Sigma.Unsafe.of_pair (c, sigma)
+            with e when to_catch e (* Hack *) ->
+              errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+        end } in
+        Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
       end }
       end
 
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index 655bfd5f5..c0cae84c0 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -102,7 +102,7 @@ let assert_ ?by c =
 
 let apply c = Tactics.apply c
 
-let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl)
+let clear id = Tactics.clear [id]
 
 let assumption = Tactics.assumption
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 090b293f5..be6ce59bd 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -34,6 +34,22 @@ open Context.Named.Declaration
 
 (* Strictness option *)
 
+let clear ids { it = goal; sigma } =
+  let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
+  let env = Goal.V82.env sigma goal in
+  let sign = Goal.V82.hyps sigma goal in
+  let cl = Goal.V82.concl sigma goal in
+  let evdref = ref (Evd.clear_metas sigma) in
+  let (hyps, concl) =
+    try Evarutil.clear_hyps_in_evi env evdref sign cl ids
+    with Evarutil.ClearDependencyError (id, _) ->
+      errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+  in
+  let sigma = !evdref in
+  let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+  let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+  { it = [gl]; sigma }
+
 let get_its_info gls = get_info gls.sigma gls.it
 
 let get_strictness,set_strictness =
@@ -469,7 +485,7 @@ let thus_tac c ctyp submetas gls =
     Proofview.V82.of_tactic (exact_check proof) gls
   else
     let refiner = concl_refiner list proof gls in
-      Tactics.refine refiner gls
+      Tacmach.refine refiner gls
 
 (* general forward step *)
 
@@ -1273,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		       (fun id ->
 			  hrec_for (out_name fix_name) per_info gls1 id)
 		       recs in
-		     generalize hrecs gls1
+		     Proofview.V82.of_tactic (generalize hrecs) gls1
 	       end;
 	       match bro with
 		   None ->
@@ -1349,7 +1365,7 @@ let end_tac et2 gls =
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
-		[generalize (pi.per_args@[pi.per_casee]);
+		[Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
 		 Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
@@ -1361,7 +1377,7 @@ let end_tac et2 gls =
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
 	  | ET_Induction,EK_dep tree ->
 	      let nargs = (List.length pi.per_args) in
-		tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
 		  begin
 		    fun gls0 ->
 		      let fix_id =
@@ -1369,7 +1385,7 @@ let end_tac et2 gls =
 		      let c_id =
 			pf_get_new_id (Id.of_string "_main_arg") gls0 in
 			tclTHENLIST
-			  [fix (Some fix_id) (succ nargs);
+			  [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
 			   tclDO nargs (Proofview.V82.of_tactic introf);
 			   Proofview.V82.of_tactic (intro_mustbe_force c_id);
 			   execute_cases (Name fix_id) pi
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0e2a40245..5eff2f277 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -135,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
-		(fun gls->generalize
+		(fun gls-> Proofview.V82.of_tactic (generalize
 		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -158,10 +158,10 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when Errors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
-		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
+		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
-		generalize [mkApp(idc,[|t|])])
+		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c05015c53..92b6e828e 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -52,13 +52,13 @@ let basename_of_global=function
   | _->assert false
 
 let clear_global=function
-    VarRef id->clear [id]
+    VarRef id-> Proofview.V82.of_tactic (clear [id])
   | _->tclIDTAC
 
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) exact_no_check
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
@@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    generalize [mkApp(id, [|left|])]));
+	    Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
 	       clear_global id;
 	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
@@ -151,9 +151,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id exact_no_check;
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
-	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
+	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
 		Proofview.V82.of_tactic introf;
 		Proofview.V82.of_tactic introf;
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls));
+		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 839586528..879145c2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -127,8 +127,7 @@ let finish_proof dynamic_infos g =
 let refine c =
   Tacmach.refine c
 
-let thin l =
-  Tacmach.thin_no_check l
+let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 
 let eq_constr u v = eq_constr_nounivs u v
 
@@ -705,7 +704,7 @@ let build_proof
 		  in
 		  tclTHENSEQ
 		    [
-		      generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
+		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
 		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
@@ -935,7 +934,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN
-    ((* observe_tac "h_generalize" *) (generalize  (List.map mkVar to_revert) ))
+    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map mkVar to_revert) )))
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
@@ -943,7 +942,7 @@ let id_of_decl decl = Nameops.out_name (get_name decl)
 let var_of_decl decl = mkVar (id_of_decl decl)
 let revert idl =
   tclTHEN
-    (generalize (List.map mkVar idl))
+    (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
     (thin idl)
 
 let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
@@ -1228,10 +1227,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	      if this_fix_info.idx + 1 = 0
 	      then tclIDTAC (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
 	      else
-		observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
+		observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1)))
 	    else
-	      Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
-		other_fix_infos 0
+	      Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+		other_fix_infos 0)
 	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
@@ -1565,7 +1564,7 @@ let prove_principle_for_gen
     Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
-    tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
+    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
@@ -1611,7 +1610,7 @@ let prove_principle_for_gen
       in
       tclTHENSEQ
 	[
-	  generalize [lemma];
+	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
 	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
@@ -1643,7 +1642,7 @@ let prove_principle_for_gen
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1));
+      (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 6a5a5ad53..72529fbbe 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -94,6 +94,7 @@ let nf_zeta =
     Environ.empty_env
     Evd.empty
 
+let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
 (* let id_to_constr id = *)
@@ -464,7 +465,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id])
+	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -714,7 +715,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  generalize (List.map mkVar ids);
+	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
 	  thin ids
 	]
       else
@@ -753,7 +754,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
 	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
@@ -936,7 +937,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -980,7 +981,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e98ac5fb5..10f08d3d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -267,8 +267,8 @@ let observe_tclTHENLIST s tacl =
 let tclUSER tac is_mes l g =
   let clear_tac =
     match l with
-      | None -> clear []
-      | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
+      | None -> tclIDTAC
+      | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l)
   in
   observe_tclTHENLIST (str "tclUSER1")
     [
@@ -399,7 +399,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
 	  observe_tclTHENLIST (str "treat_case2")[
-	    thin to_intros;
+	    Proofview.V82.of_tactic (clear to_intros);
 	    h_intros to_intros;
 	    (fun g' -> 
 	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
@@ -560,7 +560,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
 			       Proofview.V82.of_tactic default_full_auto];
 		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
-		     observe_tac (str "clearing k ") (clear [id]);
+		     observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
 		     h_intros [k;h';def];
 		     observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
 		     observe_tac (str "unfold functional")
@@ -589,7 +589,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       | (_,v_bound)::l -> 
       observe_tclTHENLIST (str "destruct_bounds_aux3")[
 	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
-	clear [v_bound];
+	Proofview.V82.of_tactic (clear [v_bound]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
 	  (fun p_hyp -> 
@@ -689,7 +689,7 @@ let mkDestructEq :
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
     observe_tclTHENLIST (str "mkDestructEq")
-     [generalize new_hyps;
+     [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
@@ -948,7 +948,7 @@ let rec destruct_hex expr_info acc l =
     | (v,hex)::l -> 
       observe_tclTHENLIST (str "destruct_hex")[
 	Proofview.V82.of_tactic (simplest_case (mkVar hex));
-	clear [hex];
+	Proofview.V82.of_tactic (clear [hex]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
 	  onNthHypId 2 (fun p -> 
@@ -1116,10 +1116,10 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
-			tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))
+			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
-		observe_tac (str "fix") (fix (Some hrec) (nargs+1));
+		observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
 		h_intros args_id;
 		Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
 		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
@@ -1306,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   observe_tclTHENLIST (str "")
 	     [
-	       generalize [lemma];
+	       Proofview.V82.of_tactic (generalize [lemma]);
 	       Proofview.V82.of_tactic (Simple.intro hid);
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5c0a8226a..0fcfbfc71 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1464,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.pf_concl gl))
    ;
-   Tactics.new_generalize env ;
+   Tactics.generalize env ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
@@ -1726,7 +1726,7 @@ let micromega_gen
      | Some (ids,ff',res') -> 
       (Tacticals.New.tclTHENLIST
 	[
-	 Tactics.new_generalize (List.map Term.mkVar ids) ;
+	 Tactics.generalize (List.map Term.mkVar ids) ;
 	 micromega_order_change  spec res' 
 	  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
 	])
@@ -1774,7 +1774,7 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.new_generalize env ;
+      Tactics.generalize env ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
   end }
@@ -1812,7 +1812,7 @@ let micromega_genr prover =
 	     (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
            (Tacticals.New.tclTHENLIST
               [
-                Tactics.new_generalize (List.map Term.mkVar ids) ;
+                Tactics.generalize (List.map Term.mkVar ids) ;
                 micromega_order_changer res' env (abstract_wrt_formula ff' ff)
               ])
   with
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 0da630530..5f906a8da 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin"
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Proofview.V82.tactic (Nsatz.nsatz_compute lt) ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
 END
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 1f420cf6a..0bf30e7fd 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -150,7 +150,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
 let generalize_tac t = generalize t
 let elim t = simplest_elim t
-let exact t = Tactics.refine t
+let exact t = Tacmach.refine t
 let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 
 let rev_assoc k =
@@ -1067,12 +1067,12 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 1;P_TYPE] in
 	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac
+	    generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
-		mkVar id1; mkVar id2 |])]);
+		mkVar id1; mkVar id2 |])];
 	    Proofview.V82.tactic (mk_then tac);
 	    (intros_using [aux]);
 	    Proofview.V82.tactic (resolve_id aux);
@@ -1104,7 +1104,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le)
+	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  let id = hyp_of_tag e1.id in
 	  let eq1 = val_of(decompile e1)
@@ -1119,20 +1119,20 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS
 	        (Tacticals.New.tclTHENLIST [
 		  (intros_using [aux]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
 		      [| eq1; rhs; mkVar aux; mkVar id |])]);
-		  Proofview.V82.tactic (clear [aux;id]);
+		  (clear [aux;id]);
 		  (intros_using [id]);
 		  (cut (mk_gt kk dd)) ])
 	        [ Tacticals.New.tclTHENS
 		    (cut (mk_gt kk izero))
 		    [ Tacticals.New.tclTHENLIST [
 		        (intros_using [aux1; aux2]);
-		        (Proofview.V82.tactic (generalize_tac
+		        (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
-			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
-		        Proofview.V82.tactic (clear [aux1;aux2;id]);
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
+		        (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
 		      Tacticals.New.tclTHENLIST [
@@ -1157,10 +1157,10 @@ let replay_history tactic_normalisation =
 	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
 		[Tacticals.New.tclTHENLIST [
 		  (intros_using [aux2;aux1]);
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
                       [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
-		  Proofview.V82.tactic (clear [aux1;aux2]);
+		  (clear [aux1;aux2]);
 		  unfold sp_not;
 		  (intros_using [aux]);
 		  Proofview.V82.tactic (resolve_id aux);
@@ -1187,10 +1187,10 @@ let replay_history tactic_normalisation =
 	      (cut state_eq)
 	      [Tacticals.New.tclTHENLIST [
 		(intros_using [aux1]);
-		Proofview.V82.tactic (generalize_tac
+		(generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
                     [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
-		Proofview.V82.tactic (clear [aux1;id]);
+		(clear [aux1;id]);
 		(intros_using [id]);
 		(loop l) ];
 	       Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
@@ -1202,10 +1202,10 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
 		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
-		   Proofview.V82.tactic (clear [aux1;aux2;id]);
+		   (clear [aux1;aux2;id]);
 		   (intros_using [id]);
 		   (loop l) ];
 		  Tacticals.New.tclTHENLIST [
@@ -1229,9 +1229,9 @@ let replay_history tactic_normalisation =
 	    (cut (mk_eq eq1 (mk_inv eq2)))
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
-	      Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
-	      Proofview.V82.tactic (clear [id1;id2;aux]);
+	      (clear [id1;id2;aux]);
 	      (intros_using [id]);
 	      (loop l) ];
             Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
@@ -1263,13 +1263,13 @@ let replay_history tactic_normalisation =
 	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
 	      (elim_id aux);
-	      Proofview.V82.tactic (clear [aux]);
+	      (clear [aux]);
 	      (intros_using [vid; aux]);
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
 	      Proofview.V82.tactic (mk_then tac);
-	      Proofview.V82.tactic (clear [aux]);
+	      (clear [aux]);
 	      (intros_using [id]);
 	      (loop l) ];
             Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
@@ -1304,7 +1304,7 @@ let replay_history tactic_normalisation =
               if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
             let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
             Tacticals.New.tclTHENLIST [
-	      Proofview.V82.tactic (generalize_tac
+	      (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
 	      Proofview.V82.tactic (mk_then tac);
 	      (intros_using [id]);
@@ -1320,12 +1320,12 @@ let replay_history tactic_normalisation =
 		 (cut (mk_gt kk2 izero))
 		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   Proofview.V82.tactic (generalize_tac
+		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
 		       eq1;eq2;kk1;kk2;
 		       mkVar aux1;mkVar aux2;
 		       mkVar id1;mkVar id2 |])]);
-		   Proofview.V82.tactic (clear [aux1;aux2]);
+		   (clear [aux1;aux2]);
 		   Proofview.V82.tactic (mk_then tac);
 		   (intros_using [id]);
 		   (loop l) ];
@@ -1338,12 +1338,12 @@ let replay_history tactic_normalisation =
                 simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+	  Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
 	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
 	  Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
+	    (generalize_tac [mkVar (hyp_of_tag e)]);
             unfold sp_Zle;
 	    simpl_in_concl;
 	    unfold sp_not;
@@ -1366,8 +1366,8 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize p_initial t in
   let shift_left =
     tclTHEN
-      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
-      (tclTRY (clear [id]))
+      (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
+      (tclTRY (Proofview.V82.of_tactic (clear [id])))
   in
   if not (List.is_empty tac) then
     let id' = new_identifier () in
@@ -1412,7 +1412,7 @@ let destructure_omega gl tac_def (id,c) =
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
-  Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id)
+  Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id)
 
 
 open Proofview.Notations
@@ -1435,7 +1435,7 @@ let coq_omega =
 	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
 	     (intros_using [v; id]);
 	     (elim_id id);
-	     Proofview.V82.tactic (clear [id]);
+	     (clear [id]);
 	     (intros_using [th;id]);
 	     tac ]),
            {kind = INEQ;
@@ -1546,7 +1546,7 @@ let nat_inject =
 	  begin try match destructurate_prop t with
               Kapp(Le,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1555,7 +1555,7 @@ let nat_inject =
                 ]
             | Kapp(Lt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1564,7 +1564,7 @@ let nat_inject =
                 ]
             | Kapp(Ge,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1573,7 +1573,7 @@ let nat_inject =
                 ]
             | Kapp(Gt,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1582,7 +1582,7 @@ let nat_inject =
                 ]
             | Kapp(Neq,[t1;t2]) ->
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac
+		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
@@ -1592,7 +1592,7 @@ let nat_inject =
             | Kapp(Eq,[typ;t1;t2]) ->
 		if is_conv typ (Lazy.force coq_nat) then
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
 		    (explore [P_APP 3; P_TYPE] t2);
@@ -1674,7 +1674,7 @@ let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
   Tacticals.New.tclTHEN
-    (Proofview.V82.tactic (tclTRY (clear [id])))
+    (Tacticals.New.tclTRY (clear [id]))
     (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id = Tacmach.New.of_old (fresh_id [] id) gl in
      Tacticals.New.tclTHEN (introduction id) (tac id)
@@ -1682,7 +1682,7 @@ let onClearedName id tac =
 
 let onClearedName2 id tac =
   Tacticals.New.tclTHEN
-    (Proofview.V82.tactic (tclTRY (clear [id])))
+    (Tacticals.New.tclTRY (clear [id]))
     (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
      let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
@@ -1723,7 +1723,7 @@ let destructure_hyps =
               then
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
-		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit))))
@@ -1734,7 +1734,7 @@ let destructure_hyps =
               begin match destructurate_prop t with
 		Kapp(Or,[t1;t2]) ->
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
                       (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit))))
@@ -1742,7 +1742,7 @@ let destructure_hyps =
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1752,7 +1752,7 @@ let destructure_hyps =
 		  let d1 = decidability t1 in
 		  let d2 = decidability t2 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1764,7 +1764,7 @@ let destructure_hyps =
 		       For t1, being decidable implies being Prop. *)
 		  let d1 = decidability t1 in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1773,7 +1773,7 @@ let destructure_hyps =
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
                   Tacticals.New.tclTHENLIST [
-		    Proofview.V82.tactic (generalize_tac
+		    (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
                   ]
@@ -1781,7 +1781,7 @@ let destructure_hyps =
 		  (try
 		     let thm = not_binop op in
                      Tacticals.New.tclTHENLIST [
-		       Proofview.V82.tactic (generalize_tac
+		       (generalize_tac
 			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 		       (onClearedName i (fun _ -> loop lit))
                      ]
@@ -1847,7 +1847,7 @@ let destructure_goal =
 	    try
 	      let dec = decidability t in
 	      Tacticals.New.tclTHEN
-                (Proofview.V82.tactic (Tactics.refine
+                (Proofview.V82.tactic (Tacmach.refine
 		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	        intro
 	    with Undecidable -> Tactics.elim_type (build_coq_False ())
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 177c870b3..dca46cbcf 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1280,8 +1280,8 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Tactics.generalize
-    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+  Proofview.V82.of_tactic (Tactics.generalize
+    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
   Proofview.V82.of_tactic (Tactics.change_concl reified) >>
   Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 2f3a3e551..73dc13e72 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -316,7 +316,7 @@ let rtauto_tac gls=
     if !check then
       Proofview.V82.of_tactic (Tactics.exact_check term) gls
     else
-      Tactics.exact_no_check term gls in
+      Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
   let tac_end_time = System.get_time () in
   let _ =
     if !check then msg_info (str "Proof term type-checking is on");
diff --git a/printing/printer.ml b/printing/printer.ml
index a16a92d0a..cb075c64f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -685,35 +685,10 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 
-  | FixRule (f,n,[],_) ->
-      (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
-  | FixRule (f,n,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,n,ar)::oth ->
-           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
-        | [] -> mt () in
-      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
-         str" with " ++ print_mut others)
-
-  | Cofix (f,[],_) ->
-      (str"cofix " ++ pr_id f)
-
-  | Cofix (f,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,ar)::oth ->
-	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
-        | [] -> mt () in
-      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
   | Refine c ->
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
-  | Thin ids ->
-      (str"clear "  ++ pr_sequence pr_id ids)
-
   | Move (id1,id2) ->
       (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 09f308abe..fd8a70c65 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -77,10 +77,10 @@ let with_check = Flags.with_option check
 
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp sign id f =
+let apply_to_hyp check sign id f =
   try apply_to_hyp sign id f
   with Hyp_not_found ->
-    if !check then error_no_such_hypothesis id
+    if check then error_no_such_hypothesis id
     else sign
 
 let check_typability env sigma c =
@@ -493,7 +493,7 @@ let convert_hyp check sign sigma d =
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp sign id
+    apply_to_hyp check sign id
       (fun _ d' _ ->
         let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
@@ -543,92 +543,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-    | FixRule (f,n,rest,j) ->
-     	let rec check_ind env k cl =
-          match kind_of_term (strip_outer_cast cl) with
-            | Prod (na,c1,b) ->
-            	if Int.equal k 1 then
-		  try
-		    fst (find_inductive env sigma c1)
-		  with Not_found ->
-		    error "Cannot do a fixpoint on a non inductive type."
-            	else
-                  let open Context.Rel.Declaration in
-		  check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b
-            | _ -> error "Not enough products."
-	in
-	let ((sp,_),u) = check_ind env n cl in
-	let firsts,lasts = List.chop j rest in
-	let all = firsts@(f,n,cl)::lasts in
-     	let rec mk_sign sign = function
-	  | (f,n,ar)::oth ->
-	      let ((sp',_),u')  = check_ind env n ar in
-	      if not (eq_mind sp sp') then
-		error "Fixpoints should be on the same mutual inductive declaration.";
-	      if !check && mem_named_context f (named_context_of_val sign) then
-		errorlabstrm "Logic.prim_refiner"
-		  (str "Name " ++ pr_id f ++ str " already used in the environment");
-	      mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth
-	  | [] ->
-	      Evd.Monad.List.map (fun (_,_,c) sigma ->
-                let gl,ev,sig' =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sig')
-              all sigma
-	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs in
-	let ids = List.map pi1 all in
-	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-	let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list (List.map pi3 all) in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-	(gls,sigma)
-
-    | Cofix (f,others,j) ->
-     	let rec check_is_coind env cl =
-	  let b = whd_betadeltaiota env sigma cl in
-          match kind_of_term b with
-            | Prod (na,c1,b) -> let open Context.Rel.Declaration in
-                                check_is_coind (push_rel (LocalAssum (na,c1)) env) b
-            | _ ->
-		try
-		  let _ = find_coinductive env sigma b in ()
-                with Not_found ->
-		  error "All methods must construct elements in coinductive types."
-	in
-	let firsts,lasts = List.chop j others in
-	let all = firsts@(f,cl)::lasts in
-     	List.iter (fun (_,c) -> check_is_coind env c) all;
-        let rec mk_sign sign = function
-          | (f,ar)::oth ->
-	      (try
-                (let _ = lookup_named_val f sign in
-                error "Name already used in the environment.")
-              with
-              |	Not_found ->
-                  mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth)
-	  | [] -> 
-              Evd.Monad.List.map (fun (_,c) sigma ->
-                let gl,ev,sigma =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sigma)
-              all sigma
-     	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs in
-	let (ids,types) = List.split all in
-	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list types in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-        (gls,sigma)
-
     | Refine c ->
 	check_meta_variables c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
@@ -636,16 +550,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
 
-    (* And now the structural rules *)
-    | Thin ids ->
-        let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-	let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
-	let (gl,ev,sigma) =
-	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
-	in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-	  ([gl], sigma)
-
     | Move (hfrom, hto) ->
   	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b4c9dae2a..ef0d52b62 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,10 +19,7 @@ open Misctypes
 
 type prim_rule =
   | Cut of bool * bool * Id.t * types
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
-  | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Thin of Id.t list
   | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 33cef7486..8c0b4ba98 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,25 +121,14 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-(* This does not check dependencies *)
-let thin_no_check ids gl =
-  if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
-
 let move_hyp_no_check id1 id2 gl =
   refiner (Move (id1,id2)) gl
 
-let mutual_fix f n others j gl =
-  with_check (refiner (FixRule (f,n,others,j))) gl
-
-let mutual_cofix f others j gl =
-  with_check (refiner (Cofix (f,others,j))) gl
-
 (* Versions with consistency checks *)
 
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let thin c             = with_check (thin_no_check c)
 let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f786b5f21..182433cb3 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,17 +86,12 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 val refiner                   : rule -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
-val thin_no_check             : Id.t list -> tactic
-val mutual_fix      :
-  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val thin             : Id.t list -> tactic
 val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 80b3fef19..ce5ef0169 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
     | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+      let rec_tac = rec_tac_initializer finite guard thms snl in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6d6e51536..9ae0ab90b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -151,7 +151,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
                begin
                 let gl'' =
                   if !to_be_cleared then
-                   tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl
+                   tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
                   else gl' in
                 id := lastid ;
                 to_be_cleared := true ;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 485559898..cfbcc4750 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -164,7 +164,7 @@ let e_give_exact flags poly (c,clenv) gl =
     else c, gl
   in
   let t1 = pf_unsafe_type_of gl c in
-    tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
+  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6bbd9b2e8..f0f408c24 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -33,7 +33,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
-     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index d441074f6..d59c2fba4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -63,7 +63,7 @@ and general_decompose_aux recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
-	  tclTHEN (Proofview.V82.tactic (clear [id]))
+	  tclTHEN (clear [id])
 	    (tclMAP (general_decompose_on_hyp recognizer)
                (ids_of_named_context bas.Tacticals.assums))))
     id
@@ -83,8 +83,8 @@ let general_decompose recognizer c =
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
 	    (ifOnHyp recognizer (general_decompose_aux recognizer)
-	      (fun id -> Proofview.V82.tactic (clear [id]))));
-       Proofview.V82.tactic (exact_no_check c) ]
+	      (fun id -> clear [id])));
+       exact_no_check c ]
   end }
 
 let head_in indl t gl =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index ef361d326..b1d3290aa 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -49,7 +49,6 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
-let clear ids = Proofview.V82.tactic (clear ids)
 let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
 
 let choose_eq eqonleft =
@@ -65,7 +64,7 @@ let choose_noteq eqonleft =
 
 let mkBranches c1 c2 =
   tclTHENLIST
-    [Proofview.V82.tactic (generalize [c2]);
+    [generalize [c2];
      Simple.elim c1;
      intros;
      onLastHyp Simple.case;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cb1d82ae6..12d31d0f3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -79,8 +79,6 @@ let _ =
 
 (* Rewriting tactics *)
 
-let clear ids = Proofview.V82.tactic (clear ids)
-
 let tclNOTSAMEGOAL tac =
   Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
 
@@ -976,7 +974,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
   tclTHENS (assert_after Anonymous absurd_term)
-    [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
+    [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -1318,7 +1316,7 @@ let inject_if_homogenous_dependent_pair ty =
        onLastHyp (fun hyp ->
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar hyp];
-           Proofview.V82.tactic (refine
+           Proofview.V82.tactic (Tacmach.refine
              (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
@@ -1364,7 +1362,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (refine pf)])
+            Proofview.V82.tactic (Tacmach.refine pf)])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
@@ -1584,7 +1582,7 @@ let substClause l2r c cls =
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
-    [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
+    [Proofview.tclUNIT (); exact_no_check c]
   end }
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 89c6beb32..3707ef90b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -30,8 +30,6 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
-let clear hyps = Proofview.V82.tactic (clear hyps)
-
 let var_occurs_in_pf gl id =
   let env = Proofview.Goal.env gl in
   occur_var env id (Proofview.Goal.concl gl) ||
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2fe4d620e..15e9d3a94 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -271,29 +271,49 @@ let replacing_dependency_msg env sigma id = function
 let error_replacing_dependency env sigma id err =
   errorlabstrm "" (replacing_dependency_msg env sigma id err)
 
-let thin l gl =
-  try Tacmach.thin l gl
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_clear_dependency (pf_env gl) (project gl) id err
+(* This tactic enables the user to remove hypotheses from the signature.
+ * Some care is taken to prevent him from removing variables that are
+ * subsequently used in other hypotheses or in the conclusion of the
+ * goal. *)
 
-let thin_for_replacing l gl =
-  try Tacmach.thin l gl
-  with Evarutil.ClearDependencyError (id,err) ->
-    error_replacing_dependency (pf_env gl) (project gl) id err
+let clear_gen fail = function
+| [] -> Proofview.tclUNIT ()
+| ids ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let ids = List.fold_right Id.Set.add ids Id.Set.empty in
+    (** clear_hyps_in_evi does not require nf terms *)
+    let gl = Proofview.Goal.assume gl in
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let concl = Proofview.Goal.concl gl in
+    let evdref = ref sigma in
+    let (hyps, concl) =
+      try clear_hyps_in_evi env evdref (named_context_val env) concl ids
+      with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+    in
+    let env = reset_with_named_context hyps env in
+    let tac = Refine.refine ~unsafe:true { run = fun sigma ->
+      Evarutil.new_evar env sigma ~principal:true concl
+    } in
+    Sigma.Unsafe.of_pair (tac, !evdref)
+  end }
+
+let clear ids = clear_gen error_clear_dependency ids
+let clear_for_replacing ids = clear_gen error_replacing_dependency ids
 
 let apply_clear_request clear_flag dft c =
   let check_isvar c =
     if not (isVar c) then
       error "keep/clear modifiers apply only to hypothesis names." in
-  let clear = match clear_flag with
+  let doclear = match clear_flag with
     | None -> dft && isVar c
     | Some true -> check_isvar c; true
     | Some false -> false in
-  if clear then Proofview.V82.tactic (thin [destVar c])
+  if doclear then clear [destVar c]
   else Tacticals.New.tclIDTAC
 
 (* Moving hypotheses *)
-let move_hyp id dest gl = Tacmach.move_hyp id dest gl
+let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
@@ -452,23 +472,120 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
 
+let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
+fun env sigma p -> function
+| [] -> Sigma ([], sigma, p)
+| arg :: rem ->
+  let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in
+  let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
+  Sigma (arg :: rem, sigma, r)
+
+let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with
+| Prod (na, c1, b) ->
+  if Int.equal k 1 then
+    try
+      let ((sp, _), u), _ = find_inductive env sigma c1 in
+      (sp, u)
+    with Not_found -> error "Cannot do a fixpoint on a non inductive type."
+  else
+    let open Context.Rel.Declaration in
+    check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| _ -> error "Not enough products."
+
 (* Refine as a fixpoint *)
-let mutual_fix = Tacmach.mutual_fix
+let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
+  let concl = Proofview.Goal.concl gl in
+  let (sp, u) = check_mutind env sigma n concl in
+  let firsts, lasts = List.chop j rest in
+  let all = firsts @ (f, n, concl) :: lasts in
+  let rec mk_sign sign = function
+  | [] -> sign
+  | (f, n, ar) :: oth ->
+    let open Context.Named.Declaration in
+    let (sp', u')  = check_mutind env sigma n ar in
+    if not (eq_mind sp sp') then
+      error "Fixpoints should be on the same mutual inductive declaration.";
+    if mem_named_context f (named_context_of_val sign) then
+      errorlabstrm "Logic.prim_refiner"
+        (str "Name " ++ pr_id f ++ str " already used in the environment");
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+  in
+  let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
+  Refine.refine { run = begin fun sigma ->
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in
+    let ids = List.map pi1 all in
+    let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
+    let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
+    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    let typarray = Array.of_list (List.map pi3 all) in
+    let bodies = Array.of_list evs in
+    let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
+    Sigma (oterm, sigma, p)
+  end }
+end }
 
-let fix ido n gl = match ido with
+let fix ido n = match ido with
   | None ->
-      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 0 gl
+    Proofview.Goal.enter { enter = begin fun gl ->
+      let name = Pfedit.get_current_proof_name () in
+      let id = new_fresh_id [] name gl in
+      mutual_fix id n [] 0
+    end }
   | Some id ->
-      mutual_fix id n [] 0 gl
+    mutual_fix id n [] 0
+
+let rec check_is_mutcoind env sigma cl =
+  let b = whd_betadeltaiota env sigma cl in
+  match kind_of_term b with
+  | Prod (na, c1, b) ->
+    let open Context.Rel.Declaration in
+    check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b
+  | _ ->
+    try
+      let _ = find_coinductive env sigma b in ()
+    with Not_found ->
+      error "All methods must construct elements in coinductive types."
 
 (* Refine as a cofixpoint *)
-let mutual_cofix = Tacmach.mutual_cofix
+let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
+  let concl = Proofview.Goal.concl gl in
+  let firsts,lasts = List.chop j others in
+  let all = firsts @ (f, concl) :: lasts in
+  List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all;
+  let rec mk_sign sign = function
+  | [] -> sign
+  | (f, ar) :: oth ->
+    let open Context.Named.Declaration in
+    if mem_named_context f (named_context_of_val sign) then
+      error "Name already used in the environment.";
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+  in
+  let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
+  Refine.refine { run = begin fun sigma ->
+    let (ids, types) = List.split all in
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in
+    let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
+    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    let typarray = Array.of_list types in
+    let bodies = Array.of_list evs in
+    let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in
+    Sigma (oterm, sigma, p)
+  end }
+end }
 
-let cofix ido gl = match ido with
+let cofix ido = match ido with
   | None ->
-      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
+    Proofview.Goal.enter { enter = begin fun gl ->
+      let name = Pfedit.get_current_proof_name () in
+      let id = new_fresh_id [] name gl in
+      mutual_cofix id [] 0
+    end }
   | Some id ->
-      mutual_cofix id [] 0 gl
+      mutual_cofix id [] 0
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
@@ -591,11 +708,11 @@ let pf_e_reduce_decl redfun where decl gl =
       let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in
       Sigma (LocalDef (id, b', ty'), sigma, p +> q)
 
-let e_reduct_in_concl (redfun, sty) =
+let e_reduct_in_concl ~check (redfun, sty) =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
-    Sigma (convert_concl_no_check c' sty, sigma, p)
+    Sigma (convert_concl ~check c' sty, sigma, p)
   end }
 
 let e_reduct_in_hyp ?(check=false) redfun (id, where) =
@@ -606,7 +723,7 @@ let e_reduct_in_hyp ?(check=false) redfun (id, where) =
 
 let e_reduct_option ?(check=false) redfun = function
   | Some id -> e_reduct_in_hyp ~check (fst redfun) id
-  | None    -> e_reduct_in_concl (revert_cast redfun)
+  | None    -> e_reduct_in_concl ~check (revert_cast redfun)
 
 (** Versions with evars to maintain the unification of universes resulting
     from conversions. *)
@@ -708,14 +825,16 @@ let change_option occl t = function
   | Some id -> change_in_hyp occl t id
   | None -> change_in_concl occl t
 
-let change chg c cls gl =
-  let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in
-  Proofview.V82.of_tactic (Tacticals.New.tclMAP (function
+let change chg c cls =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+    Tacticals.New.tclMAP (function
     | OnHyp (id,occs,where) ->
        change_option (bind_change_occurrences occs chg) c (Some (id,where))
     | OnConcl occs ->
        change_option (bind_change_occurrences occs chg) c None)
-    cls) gl
+    cls
+  end }
 
 let change_concl t = 
   change_in_concl None (make_change_arg t)
@@ -754,10 +873,9 @@ let reduce redexp cl =
   let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
   let redexps = reduction_clause redexp cl in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
-  let tac = Tacticals.New.tclMAP (fun (where,redexp) ->
+  Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
-      (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps in
-  if check then Proofview.V82.tactic (fun gl -> with_check (Proofview.V82.of_tactic tac) gl) else tac (** FIXME *)
+      (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
   end }
 
 (* Unfolding occurrences of a constant *)
@@ -789,9 +907,8 @@ let find_intro_names ctxt gl =
 let build_intro_tac id dest tac = match dest with
   | MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id)
   | dest -> Tacticals.New.tclTHENLIST 
-    [introduction id; 
-     Proofview.V82.tactic (move_hyp id dest); tac id]
-    
+    [introduction id; move_hyp id dest; tac id]
+
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -890,9 +1007,9 @@ let intro_replacing id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let next_hyp = get_next_hyp_position id gl in
   Tacticals.New.tclTHENLIST [
-    Proofview.V82.tactic (thin_for_replacing [id]);
+    clear_for_replacing [id];
     introduction id;
-    Proofview.V82.tactic (move_hyp id next_hyp);
+    move_hyp id next_hyp;
   ]
   end }
 
@@ -910,7 +1027,7 @@ let intros_possibly_replacing ids =
     let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
-	Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id])))
+	Tacticals.New.tclTRY (clear_for_replacing [id]))
 	 (if suboptimal then ids else List.rev ids))
       (Tacticals.New.tclMAP (fun (id,pos) ->
         Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
@@ -922,7 +1039,7 @@ let intros_replacing ids =
   Proofview.Goal.enter { enter = begin fun gl ->
     let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
-      (Proofview.V82.tactic (thin_for_replacing ids))
+      (clear_for_replacing ids)
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
   end }
 
@@ -979,10 +1096,14 @@ let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
 let intros_until = intros_until_gen true
 let intros_until_n = intros_until_n_gen true
 
-let tclCHECKVAR id gl = ignore (Tacmach.pf_get_hyp gl id); tclIDTAC gl
+let tclCHECKVAR id =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
+    Proofview.tclUNIT ()
+  end }
 
 let try_intros_until_id_check id =
-  Tacticals.New.tclORELSE (intros_until_id id) (Proofview.V82.tactic (tclCHECKVAR id))
+  Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id)
 
 let try_intros_until tac = function
   | NamedHyp id -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac id)
@@ -1502,9 +1623,7 @@ let solve_remaining_apply_goals =
       let concl = Proofview.Goal.concl gl in
       if Typeclasses.is_class_type evd concl then
         let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
-        let tac =
-          (Proofview.V82.tactic (Tacmach.refine_no_check c'))
-        in
+        let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in
         Sigma.Unsafe.of_pair (tac, evd')
 	else Sigma.here (Proofview.tclUNIT ()) sigma
     with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma
@@ -1563,7 +1682,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
               (fun b id ->
                 Tacticals.New.tclTHEN
                   (try_main_apply b (mkVar id))
-                  (Proofview.V82.tactic (thin [id])))
+                  (clear [id]))
               (exn0, info) c
           else
             Proofview.tclZERO ~info exn0 in
@@ -1690,7 +1809,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
         (fun id ->
           Tacticals.New.tclTHENLIST [
             apply_clear_request clear_flag false c;
-            Proofview.V82.tactic (thin idstoclear);
+            clear idstoclear;
             tac id
           ])
     with e when with_destruct && Errors.noncritical e ->
@@ -1758,7 +1877,7 @@ let cut_and_apply c =
 (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
-let new_exact_no_check c =
+let exact_no_check c =
   Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
@@ -1770,25 +1889,32 @@ let exact_check c =
   let sigma = Sigma.to_evar_map sigma in
   let sigma, ct = Typing.type_of env sigma c in
   let tac =
-      Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
+      Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
   in
   Sigma.Unsafe.of_pair (tac, sigma)
   end }
 
-let exact_no_check = Tacmach.refine_no_check
-
-let vm_cast_no_check c gl =
-  let concl = Tacmach.pf_concl gl in
-  Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
-
-let native_cast_no_check c gl =
-  let concl = Tacmach.pf_concl gl in
-  Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl
+let cast_no_check cast c =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Sigma.here (Term.mkCast (c, cast, concl)) sigma
+    end }
+  end }
 
+let vm_cast_no_check c = cast_no_check Term.VMcast c
+let native_cast_no_check c = cast_no_check Term.NATIVEcast c
 
-let exact_proof c gl =
-  let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl)
-  in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl
+let exact_proof c =
+  let open Tacmach.New in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Refine.refine { run = begin fun sigma ->
+    let sigma = Sigma.to_evar_map sigma in
+    let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
+    let sigma = Evd.merge_universe_context sigma ctx in
+    Sigma.Unsafe.of_pair (c, sigma)
+  end }
+  end }
 
 let assumption =
   let open Context.Named.Declaration in
@@ -1823,14 +1949,6 @@ let assumption =
 (*          Modification of a local context                      *)
 (*****************************************************************)
 
-(* This tactic enables the user to remove hypotheses from the signature.
- * Some care is taken to prevent him from removing variables that are
- * subsequently used in other hypotheses or in the conclusion of the
- * goal. *)
-
-let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
-  if List.is_empty ids then tclIDTAC else thin ids
-
 let on_the_bodies = function
 | [] -> assert false
 | [id] -> str " depends on the body of " ++ pr_id id
@@ -1912,13 +2030,7 @@ let clear_body ids =
   end }
 
 let clear_wildcards ids =
-  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) (project gl) (Id.of_string "_") err))
-    ids)
+  Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids
 
 (*   Takes a list of booleans, and introduces all the variables
  *  quantified in the goal which are associated with a value
@@ -1929,7 +2041,7 @@ let rec intros_clearing = function
   | (false::tl) -> Tacticals.New.tclTHEN intro (intros_clearing tl)
   | (true::tl)  ->
       Tacticals.New.tclTHENLIST
-        [ intro; Tacticals.New.onLastHypId (fun id -> Proofview.V82.tactic (clear [id])); intros_clearing tl]
+        [ intro; Tacticals.New.onLastHypId (fun id -> clear [id]); intros_clearing tl]
 
 (* Keeping only a few hypotheses *)
 
@@ -1948,7 +2060,7 @@ let keep hyps =
       else (hyp::clear,keep))
       ~init:([],[]) (Proofview.Goal.env gl)
   in
-  Proofview.V82.tactic (fun gl -> thin cl gl)
+  clear cl
   end }
 
 (*********************************)
@@ -1995,7 +2107,7 @@ let revert hyps =
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
-      (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
+      (bring_hyps ctx) <*> (clear hyps)
   end }
 
 (************************)
@@ -2137,7 +2249,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern loc ll branchsigns in
   Tacticals.New.tclTHENLASTn
-    (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
+    (Tacticals.New.tclTHEN (simplest_case c) (clear [id]))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
        nv_with_let ll)
   end }
@@ -2164,20 +2276,20 @@ let rewrite_hyp_then assert_style thin l2r id tac =
           let id' = destVar rhs in
           subst_on l2r id' lhs, early_clear id' thin
         else
-          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
           thin
     | Some (hdcncl,[c]) ->
         let l2r = not l2r in (* equality of the form eq_true *)
         if isVar c then
           let id' = destVar c in
           Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) 
-	    (Proofview.V82.tactic (clear_var_and_eq id')),
+	    (clear_var_and_eq id'),
           early_clear id' thin
         else
-          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
           thin
     | _ ->
-        Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])),
+        Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
         thin in
     (* Skip the side conditions of the rewriting step *)
     Tacticals.New.tclTHENFIRST eqtac (tac thin)
@@ -2314,7 +2426,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
         if naming = NamingMustBe (loc,id) then
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
-          Proofview.V82.tactic (clear [id]) in
+          clear [id] in
       let f = { delayed = fun env sigma ->
         let Sigma (c, sigma, p) = f.delayed env sigma in
         Sigma ((c, NoBindings), sigma, p)
@@ -2325,7 +2437,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
 and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
-      (fun id -> Proofview.V82.tactic (move_hyp id destopt))
+      (fun id -> move_hyp id destopt)
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
@@ -2558,8 +2670,7 @@ let forward b usetac ipat c =
       Proofview.Goal.enter { enter = begin fun gl ->
       let t = Tacmach.New.pf_unsafe_type_of gl c in
       let hd = head_ident c in
-      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
-	(Proofview.V82.tactic (exact_no_check c))
+      Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }
   | Some tac ->
       if b then
@@ -2618,7 +2729,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   let sigma, t = Typing.type_of env sigma c in
   generalize_goal_gen env sigma ids i o t cl
 
-let generalize_dep ?(with_let=false) c gl =
+let old_generalize_dep ?(with_let=false) c gl =
   let open Context.Named.Declaration in
   let env = pf_env gl in
   let sign = pf_hyps gl in
@@ -2653,18 +2764,22 @@ let generalize_dep ?(with_let=false) c gl =
   tclTHENLIST
     [tclEVARS evd;
      Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
-     thin (List.rev tothin')]
+     Proofview.V82.of_tactic (clear (List.rev tothin'))]
     gl
 
+let generalize_dep ?(with_let = false) c =
+  Proofview.V82.tactic (old_generalize_dep ~with_let c)
+
 (**  *)
-let generalize_gen_let lconstr gl =
+let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let newcl, evd =
-    List.fold_right_i (generalize_goal gl) 0 lconstr
-      (Tacmach.pf_concl gl,Tacmach.project gl)
+    List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
+      (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
-  Proofview.V82.of_tactic (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
-    (apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
-      if Option.is_empty b then Some c else None) lconstr))) gl
+  let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
+  let tac = apply_type newcl (List.map_filter map lconstr) in
+  Sigma.Unsafe.of_pair (tac, evd)
+end }
 
 let new_generalize_gen_let lconstr =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -2700,11 +2815,8 @@ let generalize_gen lconstr =
 let new_generalize_gen lconstr =
   new_generalize_gen_let (List.map (fun ((occs,c),na) ->
     (occs,c,None),na) lconstr)
-    
-let generalize l =
-  generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
-let new_generalize l =
+let generalize l =
   new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
@@ -2752,14 +2864,14 @@ let specialize (c,lbind) =
         (Proofview.Unsafe.tclEVARS sigma)
 	(Tacticals.New.tclTHENFIRST
 	   (assert_before_replacing id typ)
-	   (new_exact_no_check term))
+	   (exact_no_check term))
   | _ ->
       (* To deprecate in favor of generalize? *)
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma)
 	(Tacticals.New.tclTHENLAST
            (cut typ)
-           (new_exact_no_check term))
+           (exact_no_check term))
   end }
 
 (*****************************)
@@ -2789,7 +2901,7 @@ let unfold_body x =
   end }
 
 (* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (unfold_body id)) (Proofview.V82.tactic (clear [id]))
+let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
 (*****************************)
 (* High-level induction      *)
@@ -3520,18 +3632,18 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
               Tacticals.New.tclTHENLIST [
                 tac;
 		 rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
-		 Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
+		 generalize_dep ~with_let:true (mkVar oldid)]
             else Tacticals.New.tclTHENLIST [
                     tac;
-		    Proofview.V82.tactic (clear [id]);
+		    clear [id];
 		    Tacticals.New.tclDO n intro]
 	  in
 	    if List.is_empty vars then tac
 	    else Tacticals.New.tclTHEN tac
               (Tacticals.New.tclFIRST
                 [revert vars ;
-		 Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
-		      tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
+		 Tacticals.New.tclMAP (fun id ->
+		      Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars])
   end }
 
 let rec compare_upto_variables x y =
@@ -3584,17 +3696,16 @@ let specialize_eqs id gl =
   let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
-	(exact_no_check ((* refresh_universes_strict *) acc')) gl
+	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
 
 
-let specialize_eqs id gl =
-  if
-    (try ignore(clear [id] gl); false
-     with e when Errors.noncritical e -> true)
-  then
-    tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl
-  else specialize_eqs id gl
+let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let msg = str "Specialization not allowed on dependent hypotheses" in
+  Proofview.tclOR (clear [id])
+    (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
+    Proofview.V82.tactic (specialize_eqs id)
+end }
 
 let occur_rel n c =
   let res = not (noccurn n c) in
@@ -3893,10 +4004,10 @@ let recolle_clenv i params args elimclause gl =
   let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
   (* parameters correspond to first elts of lid. *)
   let clauses_params =
-    List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(i))
+    List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(i))
       0 params in
   let clauses_args =
-    List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(k+i))
+    List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(k+i))
       0 args in
   let clauses = clauses_params@clauses_args in
   (* iteration of clenv_fchain with all infos we have. *)
@@ -3906,7 +4017,7 @@ let recolle_clenv i params args elimclause gl =
       (* from_n (Some 0) means that x should be taken "as is" without
          trying to unify (which would lead to trying to apply it to
          evars if y is a product). *)
-      let indclause  = mk_clenv_from_n gl (Some 0) (x,y) in
+      let indclause  = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in
       let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
       elimclause')
     (List.rev clauses)
@@ -3916,19 +4027,20 @@ let recolle_clenv i params args elimclause gl =
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
 *)
-let induction_tac with_evars params indvars elim gl =
+let induction_tac with_evars params indvars elim =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimc = contract_letin_in_lam_header elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
-  let elimclause =
-    Tacmach.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
+  let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
-  let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  Proofview.V82.of_tactic (enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)) gl
+  let resolved = Tacmach.New.of_old (clenv_unique_resolver ~flags:(elim_flags ()) elimclause') gl in
+  enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
+  end }
 
 (* Apply induction "in place" taking into account dependent
    hypotheses from the context, replacing the main hypothesis on which
@@ -3975,7 +4087,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyp
   let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
   atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
     apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names
-      (fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim)))
+      (fun elim -> induction_tac with_evars [] [hyp0] elim))
   end }
 
 let msg_not_right_number_induction_arguments scheme =
@@ -4013,23 +4125,24 @@ let induction_without_atomization isrec with_evars elim names lid =
        but by chance, because of the addition of at least hyp0 for
        cook_sign, it behaved as if there was a real induction arg. *)
     if indvars = [] then [List.hd lid_params] else indvars in
-  let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
+  let induct_tac elim = Tacticals.New.tclTHENLIST [
     (* pattern to make the predicate appear. *)
-    Proofview.V82.of_tactic (reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl);
+    reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl;
     (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all
        possible holes using arguments given by the user (but the
        functional one). *)
     (* FIXME: Tester ca avec un principe dependant et non-dependant *)
-    induction_tac with_evars params realindvars elim
-  ]) in
+    induction_tac with_evars params realindvars elim;
+  ] in
   let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
   apply_induction_in_context None [] elim indvars names induct_tac
   end }
 
 (* assume that no occurrences are selected *)
-let clear_unselected_context id inhyps cls gl =
+let clear_unselected_context id inhyps cls =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let open Context.Named.Declaration in
-  if occur_var (Tacmach.pf_env gl) id (Tacmach.pf_concl gl) &&
+  if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
   then errorlabstrm ""
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
@@ -4041,11 +4154,12 @@ let clear_unselected_context id inhyps cls gl =
 	if Id.List.mem id' inhyps then (* if selected, do not erase *) None
 	else
 	  (* erase if not selected and dependent on id or selected hyps *)
-	  let test id = occur_var_in_decl (pf_env gl) id d in
+	  let test id = occur_var_in_decl (Tacmach.New.pf_env gl) id d in
 	  if List.exists test (id::inhyps) then Some id' else None in
-      let ids = List.map_filter to_erase (pf_hyps gl) in
-      thin ids gl
-  | None -> tclIDTAC gl
+      let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in
+      clear ids
+  | None -> Proofview.tclUNIT ()
+  end }
 
 let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let sigma = Sigma.to_evar_map sigma in
@@ -4148,7 +4262,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
         end };
         if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
         if is_arg_pure_hyp
-        then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
+        then Tacticals.New.tclTRY (clear [destVar c0])
         else Proofview.tclUNIT ();
         if isrec then Proofview.cycle (-1) else Proofview.tclUNIT ()
       ])
@@ -4202,7 +4316,7 @@ let induction_gen clear_flag isrec with_evars elim
        and w/o equality kept: no need to generalize *)
     let id = destVar c in
     Tacticals.New.tclTHEN
-      (Proofview.V82.tactic (clear_unselected_context id inhyps cls))
+      (clear_unselected_context id inhyps cls)
       (induction_with_atomization_of_ind_arg
          isrec with_evars elim names id inhyps)
   else
@@ -4730,7 +4844,7 @@ let abstract_subproof id gk tac =
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
-    new_exact_no_check (applist (lem, args))
+    exact_no_check (applist (lem, args))
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
   Sigma.Unsafe.of_pair (tac, evd)
@@ -4796,7 +4910,7 @@ end
 module New = struct
   open Proofview.Notations
 
-  let exact_proof c = Proofview.V82.tactic (exact_proof c)
+  let exact_proof c = exact_proof c
 
   open Genredexpr
   open Locus
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 4c4a96ec0..df41951c3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -30,17 +30,15 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool
 (** {6 Primitive tactics. } *)
 
 val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
-val refine          : constr -> tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
 val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
-val thin            : Id.t list -> tactic
 val mutual_fix      :
-  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
-val fix             : Id.t option -> int -> tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
-val cofix           : Id.t option -> tactic
+  Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
+val fix             : Id.t option -> int -> unit Proofview.tactic
+val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
+val cofix           : Id.t option -> unit Proofview.tactic
 
 val convert         : constr -> constr -> unit Proofview.tactic
 val convert_leq     : constr -> constr -> unit Proofview.tactic
@@ -115,11 +113,11 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic
 (** {6 Exact tactics. } *)
 
 val assumption       : unit Proofview.tactic
-val exact_no_check   : constr -> tactic
-val vm_cast_no_check : constr -> tactic
-val native_cast_no_check : constr -> tactic
+val exact_no_check   : constr -> unit Proofview.tactic
+val vm_cast_no_check : constr -> unit Proofview.tactic
+val native_cast_no_check : constr -> unit Proofview.tactic
 val exact_check      : constr -> unit Proofview.tactic
-val exact_proof      : Constrexpr.constr_expr -> tactic
+val exact_proof      : Constrexpr.constr_expr -> unit Proofview.tactic
 
 (** {6 Reduction tactics. } *)
 
@@ -155,7 +153,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
-  constr_pattern option -> change_arg -> clause -> tactic
+  constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> unit Proofview.tactic
 val reduce            : red_expr -> clause -> unit Proofview.tactic
@@ -163,7 +161,7 @@ val unfold_constr     : global_reference -> unit Proofview.tactic
 
 (** {6 Modification of the local context. } *)
 
-val clear         : Id.t list -> tactic
+val clear         : Id.t list -> unit Proofview.tactic
 val clear_body    : Id.t list -> unit Proofview.tactic
 val unfold_body   : Id.t -> unit Proofview.tactic
 val keep          : Id.t list -> unit Proofview.tactic
@@ -171,7 +169,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> unit Proofview.tactic
 
-val move_hyp      : Id.t -> Id.t move_location -> tactic
+val move_hyp      : Id.t -> Id.t move_location -> unit Proofview.tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic
@@ -384,13 +382,12 @@ val letin_pat_tac : (bool * intro_pattern_naming) option ->
 
 (** {6 Generalize tactics. } *)
 
-val generalize      : constr list -> tactic
-val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> tactic
+val generalize      : constr list -> unit Proofview.tactic
+val generalize_gen  : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic
 
-val new_generalize  : constr list -> unit Proofview.tactic
 val new_generalize_gen  : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic
 
-val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic
+val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> unit Proofview.tactic
 
 (** {6 Other tactics. } *)
 
@@ -399,7 +396,7 @@ val unify           : ?state:Names.transparent_state -> constr -> constr -> unit
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
-val specialize_eqs : Id.t -> tactic
+val specialize_eqs : Id.t -> unit Proofview.tactic
 
 val general_rewrite_clause :
   (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t
@@ -437,6 +434,4 @@ module New : sig
   val reduce_after_refine : unit Proofview.tactic
   (** The reducing tactic called after {!refine}. *)
 
-  open Proofview
-  val exact_proof : Constrexpr.constr_expr -> unit tactic
 end
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b40f61b15..23755dac1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -504,7 +504,7 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  let status = by (Tactics.New.exact_proof c) in
+  let status = by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Pp.feedback Feedback.AddedAxiom
 
@@ -861,7 +861,7 @@ let vernac_set_used_variables e =
   Proof_global.with_current_proof begin fun _ p ->
     if List.is_empty to_clear then (p, ())
     else
-      let tac = Proofview.V82.tactic (Tactics.clear to_clear) in
+      let tac = Tactics.clear to_clear in
       fst (solve SelectAll None tac p), ()
   end