Makes the new Proofview.tactic the basic type of Ltac.

On the compilation of Coq, we can see an increase of ~20% compile time on
my completely non-scientific tests. Hopefully this can be fixed.

There are a lot of low hanging fruits, but this is an iso-functionality commit.
With a few exceptions which were not necessary for the compilation of the theories:
- The declarative mode is not yet ported
- The timeout tactical is currently deactivated because it needs some subtle
I/O. The framework is ready to handle it, but I haven't done it yet.
-  For much the same reason, the ltac debugger is unplugged. It will be more
difficult, but will eventually be back.

A few comments:
I occasionnally used a coercion from [unit Proofview.tactic] to the old
[Prooftype.tactic]. It should work smoothely, but loses any backtracking
information: the coerced tactics has at most one success.
- It is used in autorewrite (it shouldn't be a problem there). Autorewrite's
code is fairly old and tricky
- It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes
as we might want to have various success in a "Hint Extern". But it would
require a heavy port of eauto.ml4
- It is used in typeclass eauto, but with a little help from Matthieu, it should
be easy to port the whole thing to the new tactic engine, actually simplifying
the code.
- It is used in fourier. I believe it to be inocuous.
- It is used in firstorder and congruence. I think it's ok. Their code is
somewhat intricate and I'm not sure they would be easy to actually port.
- It is used heavily in Function. And honestly, I have no idea whether it can do
harm or not.

Updates:
(11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based
architecture for Ltac matching (r16533), which avoid painfully and expensively
working around the exception-throwing control flow of the previous API.
(11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730)
rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN
apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma,
rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially
tclREPEAT, causing rewrites to be tried in the side-conditions of conditional
rewrites as well). The new implementation makes Coq faster, but it is
pretty much impossible to tell if it is significant at all.

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

25 files changed, 677 insertions, 603 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index b90e8ddaf..46a7e596c 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,3 +1,5 @@
+open Proofview.Notations
+
 let contrib_name = "btauto"
 
 let init_constant dir s =
@@ -214,23 +216,23 @@ module Btauto = struct
     in
     Tacticals.tclFAIL 0 msg gl
 
-  let try_unification env gl =
+  let try_unification env =
+    Goal.concl >>- fun concl ->
     let eq = Lazy.force eq in
-    let concl = Tacmach.pf_concl gl in
     let t = decomp_term concl in
     match t with
     | Term.App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
-      let tac = Tacticals.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in
-      tac gl
+      let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+      tac
     | _ ->
       let msg = str "Btauto: Internal error" in
-      Tacticals.tclFAIL 0 msg gl
+      Tacticals.New.tclFAIL 0 msg
 
-  let tac gl =
+  let tac =
+    Goal.concl >>- fun concl ->
     let eq = Lazy.force eq in
     let bool = Lazy.force Bool.typ in
-    let concl = Tacmach.pf_concl gl in
     let t = decomp_term concl in
     match t with
     | Term.App (c, [|typ; tl; tr|])
@@ -242,14 +244,14 @@ module Btauto = struct
       let fl = reify env fl in
       let fr = reify env fr in
       let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
-      Tacticals.tclTHENLIST [
-        Tactics.change_in_concl None changed_gl;
-        Tactics.apply (Lazy.force soundness);
-        Tactics.normalise_vm_in_concl;
+      Tacticals.New.tclTHENLIST [
+        Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
+        Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+        Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
         try_unification env
-      ] gl
+      ]
     | _ ->
       let msg = str "Cannot recognize a boolean equality" in
-      Tacticals.tclFAIL 0 msg gl
+      Tacticals.New.tclFAIL 0 msg
 
 end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6c578f1c2..63b6375e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,6 +23,7 @@ open Ccproof
 open Pp
 open Errors
 open Util
+open Proofview.Notations
 
 let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
@@ -244,37 +245,42 @@ let build_projection intype outtype (cstr:constructor) special default gls=
 
 let _M =mkMeta
 
-let rec proof_tac p gls =
+let rec proof_tac p : unit Proofview.tactic =
+  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
   match p.p_rule with
-      Ax c -> exact_check c gls
+      Ax c -> Proofview.V82.tactic (exact_check c)
     | SymAx c ->
-	let l=constr_of_term p.p_lhs and
-	    r=constr_of_term p.p_rhs in
-        let typ = Termops.refresh_universes (pf_type_of gls l) in
+        Proofview.V82.tactic begin fun gls ->
+	  let l=constr_of_term p.p_lhs and
+	      r=constr_of_term p.p_rhs in
+          let typ = Termops.refresh_universes (pf_type_of gls l) in
 	  exact_check
 	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+        end
     | Refl t ->
-	let lr = constr_of_term t in
-	let typ = Termops.refresh_universes (pf_type_of gls lr) in
-	exact_check
-	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+        Proofview.V82.tactic begin fun gls ->
+	  let lr = constr_of_term t in
+	  let typ = Termops.refresh_universes (pf_type_of gls lr) in
+	  exact_check
+	    (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+        end
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = Termops.refresh_universes (pf_type_of gls t2) in
+	let typ = Termops.refresh_universes (type_of t2) in
 	let prf =
 	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
-	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
+	  Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) [(proof_tac p1);(proof_tac p2)]
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = Termops.refresh_universes (pf_type_of gls tf1) in
-	let typx = Termops.refresh_universes (pf_type_of gls tx1) in
-	let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
-	let id = pf_get_new_id (Id.of_string "f") gls in
+	let typf = Termops.refresh_universes (type_of tf1) in
+	let typx = Termops.refresh_universes (type_of tx1) in
+	let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in
+        Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) >>- fun id ->
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
@@ -288,78 +294,77 @@ let rec proof_tac p gls =
 		  mkApp(tf1,[|tx1|]);
 		  mkApp(tf2,[|tx1|]);
 		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
-	  tclTHENS (refine prf)
-	    [tclTHEN (refine lemma1) (proof_tac p1);
-  	     tclFIRST
-	       [tclTHEN (refine lemma2) (proof_tac p2);
+	  Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf))
+	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma1)) (proof_tac p1);
+  	     Tacticals.New.tclFIRST
+	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma2)) (proof_tac p2);
 		reflexivity;
-		fun gls ->
-		  errorlabstrm  "Congruence"
+                Proofview.tclZERO (UserError ("Congruence" ,
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]] gls
+		       "I don't know how to handle dependent equality")))]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = Termops.refresh_universes (pf_type_of gls ti) in
-	 let outtype = Termops.refresh_universes (pf_type_of gls default) in
+	 let intype = Termops.refresh_universes (type_of ti) in
+	 let outtype = Termops.refresh_universes (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
-	 let proj=build_projection intype outtype cstr special default gls in
+         Tacmach.New.of_old (build_projection intype outtype cstr special default) >>- fun proj ->
 	 let injt=
 	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
-	   tclTHEN (refine injt) (proof_tac prf) gls
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf)
 
-let refute_tac c t1 t2 p gls =
+let refute_tac c t1 t2 p =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype = Termops.refresh_universes (pf_type_of gls tt1) in
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) >>- fun intype ->
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
-  let hid=pf_get_new_id (Id.of_string "Heq") gls in
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>- fun hid ->
   let false_t=mkApp (c,[|mkVar hid|]) in
-    tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p; simplest_elim false_t] gls
+    Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
+      [proof_tac p; simplest_elim false_t]
 
-let convert_to_goal_tac c t1 t2 p gls =
+let convert_to_goal_tac c t1 t2 p = 
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort = Termops.refresh_universes (pf_type_of gls tt2) in
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) >>- fun sort ->
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
-  let e=pf_get_new_id (Id.of_string "e") gls in
-  let x=pf_get_new_id (Id.of_string "X") gls in
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) >>- fun e ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun x ->
   let identity=mkLambda (Name x,sort,mkRel 1) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
-    tclTHENS (assert_tac (Name e) neweq)
-      [proof_tac p;exact_check endt] gls
+    Tacticals.New.tclTHENS (assert_tac (Name e) neweq)
+      [proof_tac p; Proofview.V82.tactic (exact_check endt)]
 
-let convert_to_hyp_tac c1 t1 c2 t2 p gls =
+let convert_to_hyp_tac c1 t1 c2 t2 p =
   let tt2=constr_of_term t2 in
-  let h=pf_get_new_id (Id.of_string "H") gls in
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>- fun h ->
   let false_t=mkApp (c2,[|mkVar h|]) in
-    tclTHENS (assert_tac (Name h) tt2)
+    Tacticals.New.tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
-       simplest_elim false_t] gls
+       simplest_elim false_t]
 
-let discriminate_tac cstr p gls =
+let discriminate_tac cstr p =
   let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-  let intype = Termops.refresh_universes (pf_type_of gls t1) in
-  let concl=pf_concl gls in
+  Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>- fun intype ->
+  Goal.concl >>- fun concl ->
   let outsort = mkType (Termops.new_univ ()) in
-  let xid=pf_get_new_id (Id.of_string "X") gls in
-  let tid=pf_get_new_id (Id.of_string "t") gls in
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun xid ->
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>- fun tid ->
   let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
-  let trivial=pf_type_of gls identity in
+  Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>- fun trivial ->
   let outtype = mkType (Termops.new_univ ()) in
   let pred=mkLambda(Name xid,outtype,mkRel 1) in
-  let hid=pf_get_new_id (Id.of_string "Heq") gls in
-  let proj=build_projection intype outtype cstr trivial concl gls in
+  Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>- fun hid ->
+  Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>- fun proj ->
   let injt=mkApp (Lazy.force _f_equal,
 		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|outtype;trivial;pred;identity;concl;injt|]) in
   let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
-    tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p;exact_check endt] gls
+    Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
+      [proof_tac p; Proofview.V82.tactic (exact_check endt)]
 
 (* wrap everything *)
 
@@ -370,24 +375,26 @@ let build_term_to_complete uf meta pac =
   let all_args = List.rev_append real_args dummy_args in
     applistc (mkConstruct cinfo.ci_constr) all_args
 
-let cc_tactic depth additionnal_terms gls=
+let cc_tactic depth additionnal_terms =
+  Proofview.tclUNIT () >= fun () -> (* delay for check_required_library *)
   Coqlib.check_required_library Coqlib.logic_module_name;
   let _ = debug (Pp.str "Reading subgoal ...") in
-  let state = make_prb gls depth additionnal_terms in
+  Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>- fun state ->
   let _ = debug (Pp.str "Problem built, solving ...") in
   let sol = execute true state in
   let _ = debug (Pp.str "Computation completed.") in
   let uf=forest state in
     match sol with
-	None -> tclFAIL 0 (str "congruence failed") gls
+	None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
       | Some reason ->
 	  debug (Pp.str "Goal solved, generating proof ...");
 	  match reason with
 	      Discrimination (i,ipac,j,jpac) ->
 		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
 		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-		  discriminate_tac cstr p gls
+		discriminate_tac cstr p
 	    | Incomplete ->
+                Goal.env >>- fun env ->
 		let metacnt = ref 0 in
 		let newmeta _ = incr metacnt; _M !metacnt in
 		let terms_to_complete =
@@ -404,31 +411,31 @@ let cc_tactic depth additionnal_terms gls=
 			 str "\"congruence with (" ++
 			 prlist_with_sep
 			   (fun () -> str ")" ++ spc () ++ str "(")
-			   (Termops.print_constr_env (pf_env gls))
+			   (Termops.print_constr_env env)
 			   terms_to_complete ++
 			 str ")\","
 		       end ++
 		    Pp.str "  replacing metavariables by arbitrary terms.");
-		  tclFAIL 0 (str "Incomplete") gls
+		  Tacticals.New.tclFAIL 0 (str "Incomplete")
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
 		let ta=term uf dis.lhs and tb=term uf dis.rhs in
 		  match dis.rule with
-		      Goal -> proof_tac p gls
-		    | Hyp id -> refute_tac id ta tb p gls
+		      Goal -> proof_tac p
+		    | Hyp id -> refute_tac id ta tb p
 		    | HeqG id ->
-			convert_to_goal_tac id ta tb p gls
+			convert_to_goal_tac id ta tb p
 		    | HeqnH (ida,idb) ->
-			convert_to_hyp_tac ida ta idb tb p gls
+			convert_to_hyp_tac ida ta idb tb p
 
 
 let cc_fail gls =
   errorlabstrm  "Congruence" (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
-  tclORELSE
-    (tclTHEN (tclREPEAT introf) (cc_tactic depth l))
-    cc_fail
+  Tacticals.New.tclORELSE
+    (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
+    (Proofview.V82.tactic cc_fail)
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
    might be slow now, let's rather do something equivalent
@@ -443,22 +450,31 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
    the fact that congruence is called internally.
 *)
 
-let f_equal gl =
+let f_equal =
+  Goal.concl >>- fun concl ->
+  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
   let cut_eq c1 c2 =
-    let ty = Termops.refresh_universes (pf_type_of gl c1) in
-    tclTHENTRY
-      (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
-      (simple_reflexivity ())
+    let ty = Termops.refresh_universes (type_of c1) in
+    Proofview.V82.tactic begin
+      tclTHENTRY
+        (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
+        (simple_reflexivity ())
+    end
   in
-  try match kind_of_term (pf_concl gl) with
+  Proofview.tclORELSE
+    begin match kind_of_term concl with
     | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
 	begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
-		if i < 0 then tclTRY (congruence_tac 1000 [])
-		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
-	      in cuts (Array.length v - 1) gl
-	  | _ -> tclIDTAC gl
+		if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
+		else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+	      in cuts (Array.length v - 1)
+	  | _ -> Proofview.tclUNIT ()
 	end
-    | _ -> tclIDTAC gl
-  with Type_errors.TypeError _ -> tclIDTAC gl
+    | _ -> Proofview.tclUNIT ()
+    end
+    begin function
+      | Type_errors.TypeError _ -> Proofview.tclUNIT ()
+      | e -> Proofview.tclZERO e
+    end
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 365c172c9..a022a07da 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -9,12 +9,12 @@
 open Term
 open Proof_type
 
-val proof_tac: Ccproof.proof -> Proof_type.tactic
+val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
-val cc_tactic : int -> constr list -> tactic
+val cc_tactic : int -> constr list ->  unit Proofview.tactic
 
 val cc_fail : tactic
 
-val congruence_tac : int -> constr list -> tactic
+val congruence_tac : int -> constr list -> unit Proofview.tactic
 
-val f_equal : tactic
+val f_equal : unit Proofview.tactic
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 30ed01c49..3b8487d75 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -121,7 +121,7 @@ let start_proof_tac gls=
   tcl_change_info info gls
 
 let go_to_proof_mode () =
-  Pfedit.by start_proof_tac;
+  Pfedit.by (Proofview.V82.tactic start_proof_tac);
   let p = Proof_global.give_me_the_proof () in
   Decl_mode.focus p
 
@@ -214,7 +214,8 @@ let filter_hyps f gls =
 
 let local_hyp_prefix = Id.of_string "___"
 
-let add_justification_hyps keep items gls =
+let add_justification_hyps keep items gls = assert false
+(* arnaud: todo
   let add_aux c gls=
     match kind_of_term c with
 	Var id ->
@@ -226,6 +227,7 @@ let add_justification_hyps keep items gls =
 	    tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere)
               (thin_body [id]) gls in
     tclMAP add_aux items gls
+*)
 
 let prepare_goal items gls =
   let tokeep = ref Id.Set.empty in
@@ -235,11 +237,11 @@ let prepare_goal items gls =
        filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
 
 let my_automation_tac = ref
-  (fun gls -> anomaly (Pp.str "No automation registered"))
+  (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
 
 let register_automation_tac tac = my_automation_tac:= tac
 
-let automation_tac gls = !my_automation_tac gls
+let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
 
 let justification tac gls=
     tclORELSE
@@ -253,8 +255,10 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification elems gls=
+let default_justification elems gls= assert false
+(* arnaud: todo
   justification (tclTHEN (prepare_goal elems) automation_tac) gls
+*)
 
 (* code for conclusion refining *)
 
@@ -452,7 +456,8 @@ let mk_stat_or_thesis info gls = function
       error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
-let just_tac _then cut info gls0 = 
+let just_tac _then cut info gls0 = assert false
+(* arnaud: todo
   let last_item =
     if _then then
       try [mkVar (get_last (pf_env gls0))]
@@ -471,8 +476,10 @@ let just_tac _then cut info gls0 =
       | Some tac ->
 	  (Tacinterp.eval_tactic tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
+*)
 
-let instr_cut mkstat _thus _then cut gls0 =
+let instr_cut mkstat _thus _then cut gls0 = assert false
+(* arnaud:
   let info = get_its_info gls0 in
   let stat = cut.cut_stat in
   let (c_id,_) = match stat.st_label with
@@ -487,7 +494,7 @@ let instr_cut mkstat _thus _then cut gls0 =
     tclTHENS (assert_postpone c_id c_stat)
       [tclTHEN tcl_erase_info (just_tac _then cut info);
        thus_tac] gls0
-
+*)
 
 
 (* iterated equality *)
@@ -505,7 +512,8 @@ let decompose_eq id gls =
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
 
-let instr_rew _thus rew_side cut gls0 =
+let instr_rew _thus rew_side cut gls0 = assert false
+(* arnaud:
   let last_id =
     try get_last (pf_env gls0)
     with UserError _ -> error "No previous equality."
@@ -546,12 +554,13 @@ let instr_rew _thus rew_side cut gls0 =
 		 (tclTHENS (transitivity rhs)
 		    [exact_check (mkVar last_id);just_tac]);
 	       thus_tac new_eq] gls0
-
+*)
 
 
 (* tactics for claim/focus *)
 
-let instr_claim _thus st gls0 =
+let instr_claim _thus st gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let (id,_) = match st.st_label with
       Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
@@ -565,10 +574,12 @@ let instr_claim _thus st gls0 =
     tclTHENS (assert_postpone id st.st_it)
       [thus_tac;
        tcl_change_info ninfo1] gls0
+*)
 
 (* tactics for assume *)
 
-let push_intro_tac coerce nam gls =
+let push_intro_tac coerce nam gls = assert false
+(* arnaud: todo
       let (hid,_) =
 	match nam with
 	    Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
@@ -577,6 +588,7 @@ let push_intro_tac coerce nam gls =
 	  [intro_mustbe_force hid;
 	   coerce hid]
 	  gls
+*)
 
 let assume_tac hyps gls =
   List.fold_right
@@ -643,7 +655,8 @@ let rec build_applist prod = function
       let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
-let instr_suffices _then cut gls0 =
+let instr_suffices _then cut gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
@@ -659,6 +672,7 @@ let instr_suffices _then cut gls0 =
 	   tcl_erase_info;
 	   just_tac _then cut info];
       thus_tac] gls0
+*)
 
 (* tactics for consider/given *)
 
@@ -678,7 +692,8 @@ let conjunction_arity id gls =
 	    List.length rc
       | _ -> raise Not_found
 
-let rec intron_then n ids ltac gls =
+let rec intron_then n ids ltac gls = assert false
+(* arnaud:
   if n<=0 then
     ltac ids gls
   else
@@ -686,9 +701,11 @@ let rec intron_then n ids ltac gls =
       tclTHEN
 	(intro_mustbe_force id)
 	(intron_then (pred n) (id::ids) ltac) gls
+*)
 
 
-let rec consider_match may_intro introduced available expected gls =
+let rec consider_match may_intro introduced available expected gls = assert false
+(* arnaud:
   match available,expected with
       [],[] ->
 	  tclIDTAC gls
@@ -731,8 +748,10 @@ let rec consider_match may_intro introduced available expected gls =
 			 (List.rev_append l rest_ids) expected)] gls)
 	  end
 	  gls
+*)
 
-let consider_tac c hyps gls =
+let consider_tac c hyps gls = assert false
+(* arnaud: todo
   match kind_of_term (strip_outer_cast c) with
       Var id ->
 	consider_match false [] [id] hyps gls
@@ -741,6 +760,7 @@ let consider_tac c hyps gls =
 	tclTHEN
 	  (forward None (Some (Loc.ghost, IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls
+*)
 
 
 let given_tac hyps gls =
@@ -768,9 +788,11 @@ let rec build_function args body =
 	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
     | [] -> body
 
-let define_tac id args body gls =
+let define_tac id args body gls = assert false
+(* arnaud: todo:
   let t = build_function args body in
     letin_tac None (Name id) t None Locusops.nowhere gls
+*)
 
 (* tactics for reconsider *)
 
@@ -903,7 +925,8 @@ let register_nodep_subcase id= function
       end
   | _ -> anomaly (Pp.str "wrong stack state")
 
-let suppose_tac hyps gls0 =
+let suppose_tac hyps gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
@@ -916,6 +939,7 @@ let suppose_tac hyps gls0 =
 		    assume_tac hyps;
 		    clear old_clauses];
        tcl_change_info ninfo2] gls0
+*)
 
 (* suppose it is ... *)
 
@@ -1104,7 +1128,8 @@ let rec register_dep_subcase id env per_info pat = function
 	(EK_dep (start_tree env per_info.per_ind per_info.per_wf))
   | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree)
 
-let case_tac params pat_info hyps gls0 =
+let case_tac params pat_info hyps gls0 = assert false
+(* arnaud: todo
   let info = get_its_info gls0 in
   let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
@@ -1125,6 +1150,7 @@ let case_tac params pat_info hyps gls0 =
 	  assume_hyps_or_theses hyps;
 	  clear old_clauses];
        tcl_change_info ninfo2] gls0
+*)
 
 (* end cases *)
 
@@ -1179,7 +1205,8 @@ let hrec_for fix_id per_info gls obj_id =
     compose_lam rc (whd_beta gls.sigma hd2)
 
 
-let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
+let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = assert false
+(* arnaud: todo
   match tree, objs  with
       Close_patt t,_ ->
 	let args0 = pop_stacks args in
@@ -1272,6 +1299,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
     | End_patt (_,_) , _ :: _  ->
 	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
+*)
 
 let understand_my_constr c gls =
   let env = pf_env gls in
@@ -1283,13 +1311,16 @@ let understand_my_constr c gls =
   in
   Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
 
-let my_refine c gls =
+let my_refine c gls = assert false
+(* arnaud: todo
   let oc = understand_my_constr c gls in
   Refine.refine oc gls
+*)
 
 (* end focus/claim *)
 
-let end_tac et2 gls =
+let end_tac et2 gls = assert false
+(* arnaud: todo
   let info = get_its_info gls in
   let et1,pi,ek,clauses =
     match info.pm_stack with
@@ -1354,6 +1385,7 @@ let end_tac et2 gls =
 			     [mkVar c_id]  0 tree] gls0
 		  end
       end gls
+*)
 
 (* escape *)
 
@@ -1463,7 +1495,7 @@ let do_instr raw_instr pts =
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
-      Pfedit.by (tclTHEN (eval_instr instr) clean_tmp)
+      Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))
     else () end;
   postprocess pts raw_instr.instr;
   (* spiwack: this should restore a compatible semantics with
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 107b65366..d78ca84d1 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -15,9 +15,9 @@ open Decl_mode
 val go_to_proof_mode: unit -> unit
 val return_from_tactic_mode: unit -> unit
 
-val register_automation_tac: tactic -> unit
+val register_automation_tac: unit Proofview.tactic -> unit
 
-val automation_tac : tactic
+val automation_tac : unit Proofview.tactic
 
 val concl_refiner:
   Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 84060dc9d..c125be65a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -79,7 +79,7 @@ let gen_ground_tac flag taco ids bases gl=
       let startseq gl=
 	let seq=empty_seq !ground_depth in
 	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
-      let result=ground_tac solver startseq gl in
+      let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
 	qflag:=backup;result
     with reraise -> qflag:=backup;raise reraise
 
@@ -125,29 +125,31 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) l [] ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) [] l ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (Option.map eval_tactic t) [] [] ]
+     [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
 END
 
+open Proofview.Notations
 
-let default_declarative_automation gls =
-  tclORELSE
-    (tclORELSE (Auto.h_trivial [] None)
+let default_declarative_automation =
+  Proofview.tclUNIT () >= fun () -> (* delay for [congruence_depth] *)
+  Tacticals.New.tclORELSE
+    (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
     (Cctac.congruence_tac !congruence_depth []))
-    (gen_ground_tac true
-       (Some (tclTHEN
+    (Proofview.V82.tactic (gen_ground_tac true
+       (Some (Tacticals.New.tclTHEN
 		(snd (default_solver ()))
 		(Cctac.congruence_tac !congruence_depth [])))
-       [] []) gls
+       [] []))
 
 
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ac612d0cd..0acdc4c80 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -143,11 +143,11 @@ let left_instance_tac (inst,id) continue seq=
 	else
 	  tclTHENS (cut dom)
 	    [tclTHENLIST
-	       [introf;
+	       [Proofview.V82.of_tactic introf;
 		(fun gls->generalize
 		   [mkApp(constr_of_global id,
 			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		introf;
+		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
 	    tclTRY assumption]
@@ -168,7 +168,7 @@ let left_instance_tac (inst,id) continue seq=
 	  in
 	    tclTHENLIST
 	      [special_generalize;
-	       introf;
+	       Proofview.V82.of_tactic introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
 
@@ -177,14 +177,14 @@ let right_instance_tac inst continue seq=
       Phantom dom ->
 	tclTHENS (cut dom)
 	[tclTHENLIST
-	   [introf;
+	   [Proofview.V82.of_tactic introf;
 	    (fun gls->
-	       split (ImplicitBindings
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	       Proofview.V82.of_tactic (split (ImplicitBindings
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (split (ImplicitBindings [t]))
+	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 02a0dd20d..99e03cdbe 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -67,24 +67,24 @@ let ll_atom_tac a backtrack id continue seq=
 	[generalize [mkApp(constr_of_global id,
 			   [|constr_of_global (find_left a seq)|])];
 	 clear_global id;
-	 intro]
+	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
     (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
 
 let and_tac backtrack continue seq=
-  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
+  tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack
 
 let or_tac backtrack continue seq=
   tclORELSE
-    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
+    (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq))))))
     backtrack
 
 let arrow_tac backtrack continue seq=
-  tclIFTHENELSE intro (wrap 1 true continue seq)
+  tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq)
     (tclORELSE
-       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
+       (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq)))
        backtrack)
 (* left connectives rules *)
 
@@ -92,9 +92,9 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [simplest_elim (constr_of_global id);
+      [Proofview.V82.of_tactic (simplest_elim (constr_of_global id));
        clear_global id;
-       tclDO n intro])
+       tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
      backtrack gls
 
@@ -103,15 +103,15 @@ let left_or_tac ind backtrack id continue seq gls=
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n intro;
+       tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (simplest_elim (constr_of_global id))
+      (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  simplest_elim (constr_of_global id)
+  Proofview.V82.of_tactic (simplest_elim (constr_of_global id))
 
 (* left arrow connective rules *)
 
@@ -135,7 +135,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
 	   (tclTHENLIST
 	      [generalize newhyps;
 	       clear_global id;
-	       tclDO lp intro])
+	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
@@ -146,7 +146,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
     tclORELSE
       (tclTHENS (cut c)
 	 [tclTHENLIST
-	    [introf;
+	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (cut cc)
@@ -154,8 +154,8 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     tclTHENLIST
 	       [generalize [d];
 		clear_global id;
-		introf;
-		introf;
+		Proofview.V82.of_tactic introf;
+		Proofview.V82.of_tactic introf;
 		tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
@@ -163,9 +163,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 
 let forall_tac backtrack continue seq=
   tclORELSE
-    (tclIFTHENELSE intro (wrap 0 true continue seq)
+    (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq)
        (tclORELSE
-	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+	  (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
@@ -175,9 +175,9 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (simplest_elim (constr_of_global id))
+      (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
       (tclTHENLIST [clear_global id;
-                    tclDO n intro;
+                    tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
       backtrack
       gls
@@ -186,13 +186,13 @@ let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
     (tclTHENS (cut prod)
        [tclTHENLIST
-	  [intro;
+	  [Proofview.V82.of_tactic intro;
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
 	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
 		tclTHEN (generalize [term]) (clear [id0]) gls);
 	   clear_global id;
-	   intro;
+	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
 	tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 3dd384ee8..d49f225e6 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -478,22 +478,22 @@ let rec fourier gl=
 	     "Rlt" ->
 	       (tclTHEN
 	         (tclTHEN (apply (get coq_Rfourier_not_ge_lt))
-			  (intro_using  fhyp))
+			  (Proofview.V82.of_tactic (intro_using  fhyp)))
 		 fourier)
 	    |"Rle" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_gt_le))
-		       (intro_using  fhyp))
+		       (Proofview.V82.of_tactic (intro_using  fhyp)))
 			fourier)
 	    |"Rgt" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_le_gt))
-		       (intro_using  fhyp))
+		       (Proofview.V82.of_tactic (intro_using  fhyp)))
 	      fourier)
 	    |"Rge" ->
 	     (tclTHEN
 	      (tclTHEN (apply (get coq_Rfourier_not_lt_ge))
-		       (intro_using  fhyp))
+		       (Proofview.V82.of_tactic (intro_using  fhyp)))
 	      fourier)
 	    |_-> raise GoalDone)
         |_-> raise GoalDone
@@ -595,16 +595,16 @@ let rec fourier gl=
 				       ))
 		      (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
-			    (tclTHENS (Equality.replace
+			    (tclTHENS (Proofview.V82.of_tactic (Equality.replace
 				       (mkAppL [|get coq_Rminus;!t2;!t1|]
 					       )
-				       tc)
+				       tc))
 		 	       [tac2;
                                 (tclTHENS
-				  (Equality.replace
+				  (Proofview.V82.of_tactic (Equality.replace
 				    (mkApp (get coq_Rinv,
 				      [|get coq_R1|]))
-				    (get coq_R1))
+				    (get coq_R1)))
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
       			        [tclORELSE
@@ -617,7 +617,7 @@ let rec fourier gl=
 				]));
                        !tac1]);
 	   tac:=(tclTHENS (cut (get coq_False))
-				  [tclTHEN intro (contradiction None);
+				  [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None));
 				   !tac])
       |_-> assert false) |_-> assert false
 	  );
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 01166d1db..1635cecc0 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -11,5 +11,5 @@
 open FourierR
 
 TACTIC EXTEND fourier
-  [ "fourierz" ] -> [ fourier ]
+  [ "fourierz" ] -> [ Proofview.V82.tactic fourier ]
 END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8edb16850..2da4b6147 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -175,7 +175,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g ->
     let prov_id = pf_get_new_id hyp_id g in
     tclTHENS
-      ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
+      ((* observe_tac msg *) Proofview.V82.of_tactic (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac))))
       [tclTHENLIST
       [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -189,7 +189,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
   let nb_intros = List.length context in
   tclTHENLIST
     [
-      tclDO nb_intros intro; (* introducing context *)
+      tclDO nb_intros (Proofview.V82.of_tactic intro); (* introducing context *)
       (fun g ->
 	 let context_hyps =
 	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
@@ -322,7 +322,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
     in
     let prove_new_hyp : tactic =
       tclTHEN
-	(tclDO ctxt_size intro)
+	(tclDO ctxt_size (Proofview.V82.of_tactic intro))
 	(fun g ->
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
@@ -395,7 +395,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
 	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
-	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
 	      (do_rewrite eq_ids)
 	      g
   in
@@ -433,7 +433,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	      let context_length = List.length context in
 	      tclTHENLIST
 		[
-		  tclDO context_length intro;
+		  tclDO context_length (Proofview.V82.of_tactic intro);
 		  (fun g ->
 		     let context_hyps_ids =
 		       fst (list_chop ~msg:"rec hyp : context_hyps"
@@ -447,7 +447,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_tac (Name rec_pte_id) t_x)
+		       (Proofview.V82.of_tactic (assert_tac (Name rec_pte_id) t_x))
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -484,7 +484,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  let prove_trivial =
 	    let nb_intro = List.length context in
 	    tclTHENLIST [
-	      tclDO nb_intro intro;
+	      tclDO nb_intro (Proofview.V82.of_tactic intro);
 	      (fun g ->
 		 let context_hyps =
 		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
@@ -583,9 +583,9 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
     tclTHENLIST
       [
 	(* We first introduce the variables *)
-	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps));
 	(* Then the equation itself *)
-	intro_using heq_id;
+	Proofview.V82.of_tactic (intro_using heq_id);
 	onLastHypId (fun heq_id -> tclTHENLIST [
 	(* Then the new hypothesis *)
 	tclMAP introduction_no_check dyn_infos.rec_hyps;
@@ -636,7 +636,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
+	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -704,7 +704,7 @@ let build_proof
 		      thin dyn_infos.rec_hyps;
 		      pattern_option [Locus.AllOccurrencesBut [1],t] None;
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [h_simplest_case t;
+			 tclTHENSEQ [Proofview.V82.of_tactic (h_simplest_case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -729,7 +729,7 @@ let build_proof
 		match kind_of_term( pf_concl g) with
 		  | Prod _ ->
 		      tclTHEN
-			intro
+			(Proofview.V82.of_tactic intro)
 			(fun g' ->
 			   let (id,_,_) = pf_last_hyp g' in
 			   let new_term =
@@ -965,13 +965,13 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let prove_replacement =
     tclTHENSEQ
       [
-	tclDO (nb_params + rec_args_num + 1) intro;
+	tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
 	(* observe_tac "" *) (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings));
-	      intros_reflexivity] g
+	      (* observe_tac "h_case" *) (Proofview.V82.of_tactic (h_case false (mkVar rec_id,NoBindings)));
+	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
   in
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
     (fun _ _ -> ());
-  Pfedit.by (prove_replacement);
+  Pfedit.by (Proofview.V82.tactic prove_replacement);
   Lemmas.save_named false
 
 
@@ -1019,12 +1019,12 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
-      (tclDO nb_intro_to_do intro)
+      (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
       (
 	fun g' ->
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
 	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
-	  tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g'
       )
       g
 
@@ -1206,9 +1206,9 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
-	[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params));
-	  (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates));
-	  (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches));
+	[ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params));
+	  (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates));
+	  (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches));
 	  (* observe_tac "building fixes" *) mk_fixes;
 	]
     in
@@ -1225,7 +1225,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
 	    [
-	      (* observe_tac ("introducing args") *) (tclDO nb_args intro);
+	      (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro));
 	      (fun g -> (* replacement of the function by its body *)
 		 let args = nLastDecls nb_args g in
 		 let fix_body = fix_info.body_with_param in
@@ -1289,7 +1289,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
 	  tclTHENSEQ
 	    [
-	      tclDO nb_args intro;
+	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
 		 let args = nLastDecls nb_args g in
 		 let args_id = List.map (fun (id,_,_) -> id) args in
@@ -1386,7 +1386,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
     let eqs = List.map mkVar eqs in
     let rewrite =
-      tclFIRST (List.map Equality.rewriteRL eqs )
+      tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
     let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in
     let f_app = Array.last (snd (destApp hrec_concl)) in
@@ -1411,8 +1411,8 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl ->
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
-		    (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences
-			       true (* dep proofs also: *) true id (mkVar eq) false))
+		    (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences
+			       true (* dep proofs also: *) true id (mkVar eq) false)))
 		    gl
 	       )
 	       eqs
@@ -1543,9 +1543,9 @@ let prove_principle_for_gen
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
-	       (assert_by (Name wf_thm_id)
+	       (Proofview.V82.of_tactic (assert_by (Name wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
+		  (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
@@ -1583,8 +1583,8 @@ let prove_principle_for_gen
       tclTHENSEQ
 	[
 	  generalize [lemma];
-	  h_intro hid;
-	  Elim.h_decompose_and (mkVar hid);
+	  Proofview.V82.of_tactic (h_intro hid);
+	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
@@ -1606,10 +1606,10 @@ let prove_principle_for_gen
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
-      (* observe_tac "" *) (assert_by
+      (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
 	 (Name acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
-	 (prove_rec_arg_acc)
+	 (Proofview.V82.tactic prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
@@ -1617,7 +1617,7 @@ let prove_principle_for_gen
       (* observe_tac "h_fix " *) (h_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_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
-      Equality.rewriteLR (mkConst eq_ref);
+      Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
 	   let _,args = destApp (pf_concl gl') in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e5d8fe4c1..0850d556c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
       (hook new_principle_type)
     ;
     (*       let _tim1 = System.get_time ()  in *)
-    Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
+    Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e65ca94f0..b317cec0d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -71,7 +71,7 @@ END
 TACTIC EXTEND newfuninv
    [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
      [
-       Invfun.invfun hyp fname
+       Proofview.V82.tactic (Invfun.invfun hyp fname)
      ]
 END
 
@@ -98,7 +98,7 @@ TACTIC EXTEND newfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x pat)) princl ]
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
@@ -109,7 +109,7 @@ TACTIC EXTEND snewfunind
 	 | [c] -> c
 	 | c::cl -> applist(c,cl)
        in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
+       Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x pat)) princl ]
 END
 
 
@@ -318,10 +318,10 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)
+    (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
     (tclTHENFIRST
-      (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
-      Tactics.reflexivity)
+      (Proofview.V82.of_tactic (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)))
+      (Proofview.V82.of_tactic Tactics.reflexivity))
     gl
 
 
@@ -432,7 +432,7 @@ TACTIC EXTEND finduction
 	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
 	  | _ ->
 	      let heuristic = chose_heuristic oi in
-	      finduction (Some id) heuristic tclIDTAC
+	      Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
       ]
 END
 
@@ -442,13 +442,13 @@ TACTIC EXTEND fauto
     [ "fauto" tactic(tac)] ->
       [
 	let heuristic = chose_heuristic None in
-	finduction None heuristic (Tacinterp.eval_tactic tac)
+	Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
       ]
   |
     [ "fauto" ] ->
       [
 	let heuristic = chose_heuristic None in
-	finduction None heuristic tclIDTAC
+	Proofview.V82.tactic (finduction None heuristic tclIDTAC)
       ]
 
 END
@@ -456,7 +456,7 @@ END
 
 TACTIC EXTEND poseq
   [ "poseq" ident(x) constr(c) ] ->
-      [ poseq x c ]
+      [ Proofview.V82.tactic (poseq x c) ]
 END
 
 VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 34814c350..4f32feb24 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -105,18 +105,18 @@ let functional_induction with_clean c princl pat =
 	    }
 	in
 	Tacticals.tclTHEN
-	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl )
+	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
 	  (Hiddentac.h_reduce flag Locusops.allHypsAndConcl)
 	  g
       else Tacticals.tclIDTAC g
     in
     Tacticals.tclTHEN
-      (choose_dest_or_ind
+      (Proofview.V82.of_tactic (choose_dest_or_ind
 	 princ_infos
 	 args_as_induction_constr
 	 princ'
 	 (None,pat)
-         None)
+         None))
       subst_and_reduce
       g
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 04cc139c0..e5b975e14 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -484,7 +484,7 @@ let jmeq_refl () =
   with e when Errors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
-  tclMAP h_intro l
+  tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) l
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
@@ -503,5 +503,5 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
 let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
   tclREPEAT
     (List.fold_right
-       (fun (eq,b) i -> tclORELSE ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i)
+       (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4f7a61fbf..ce25f7aaf 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -399,7 +399,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
 					       match l with 
 						 | [] -> tclIDTAC 
-						 | _ -> h_intro_patterns l);
+						 | _ -> Proofview.V82.of_tactic (h_intro_patterns l));
 	    (* unfolding of all the defined variables introduced by this branch *)
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
@@ -414,9 +414,9 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	    observe_tac ("toto ") tclIDTAC;
     
 	    (* introducing the the result of the graph and the equality hypothesis *)
-	    observe_tac "introducing" (tclMAP h_intro [res;hres]);
+	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g -> h_exact (app_constructor g) g)  
 	  ]
@@ -466,11 +466,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     in
     tclTHENSEQ
       [ 
-	observe_tac "principle" (assert_by
+	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (h_exact f_principle));
-	observe_tac "intro args_names" (tclMAP h_intro args_names);
+	  (Proofview.V82.tactic (h_exact f_principle))));
+	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
@@ -741,7 +741,7 @@ and intros_with_rewrite_aux : tactic =
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
 			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
@@ -759,18 +759,18 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id;
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
 				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Equality.rewriteLR (mkVar id));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
 		      else if isVar args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ h_intro id;
+			tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);
 				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Equality.rewriteRL (mkVar id));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -778,16 +778,16 @@ and intros_with_rewrite_aux : tactic =
 			begin
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
-			    h_intro id;
-			    tclTRY (Equality.rewriteLR (mkVar id));
+			    Proofview.V82.of_tactic (h_intro id);
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
 		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
-		      Tauto.tauto g
+		      Proofview.V82.of_tactic Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			h_case false (v,NoBindings);
+			Proofview.V82.of_tactic (h_case false (v,NoBindings));
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -803,7 +803,7 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		  | _ ->
 		      let id = pf_get_new_id (Id.of_string "y") g  in
-		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+		      tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
 	      tclTHENSEQ[
@@ -824,12 +824,12 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      h_case false (v,NoBindings);
-	      intros;
+	      Proofview.V82.of_tactic (h_case false (v,NoBindings));
+	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
-	| _ -> reflexivity
-    with e when Errors.noncritical e -> reflexivity
+        | _ -> Proofview.V82.of_tactic reflexivity
+    with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
@@ -841,15 +841,15 @@ let rec reflexivity_with_destruct_cases g =
 	       match kind_of_term  (pf_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
-		     then Equality.discrHyp id g
+		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite]  g
+		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
   in
   (tclFIRST
-    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity;
+    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity);
       observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
       (*  We reach this point ONLY if
 	  the same value is matched (at least) two times
@@ -948,8 +948,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
 	in
 	tclTHENSEQ[
-	  tclMAP h_intro ids;
-	  Equality.rewriteLR (mkConst eq_lemma);
+	  tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) ids;
+	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  h_reduce
@@ -996,12 +996,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let params_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar params_names in
     tclTHENSEQ
-      [ tclMAP h_intro (args_names@[res;hres]);
+      [ tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
 	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
-	h_intro graph_principle_id;
+	Proofview.V82.of_tactic (h_intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -1070,8 +1070,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-	      (proving_tac i));
+	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
+	      (proving_tac i)));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1121,8 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
            (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i));
+	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+	      (proving_tac i)));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
 	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1162,7 +1162,7 @@ let revert_graph kn post_tac hid g =
 		    [
 		      h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
 		      thin [hid];
-		      h_intro hid;
+		      Proofview.V82.of_tactic (h_intro hid);
 		      post_tac hid
 		    ]
 		    g
@@ -1197,7 +1197,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
 	      | App(f,f_args),_ when eq_constr f fconst ->
-		  ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2))
+		  ((fun hid -> Proofview.V82.of_tactic (h_symmetry (Locusops.onHyp hid))),f_args,args.(2))
 	      |_,App(f,f_args) when eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
@@ -1206,8 +1206,8 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    pre_tac hid;
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
-	    h_intro hid;
-	    Inv.inv FullInversion None (NamedHyp hid);
+	    Proofview.V82.of_tactic (h_intro hid);
+	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
@@ -1228,7 +1228,9 @@ let invfun qhyp f  =
     let f_correct = mkConst(Option.get finfos.correctness_lemma)
     and kn = fst finfos.graph_ind
     in
-    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
+    Proofview.V82.of_tactic (
+      Tactics.try_intros_until (fun hid -> Proofview.V82.tactic (functional_inversion kn hid (mkConst f)  f_correct)) qhyp
+    )
   with
     | Not_found ->  error "No graph found"
     | Option.IsNone  -> error "Cannot use equivalence with graph!"
@@ -1238,8 +1240,9 @@ let invfun qhyp f g =
   match f with
     | Some f -> invfun qhyp f g
     | None ->
+        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
-	  (fun hid g ->
+	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_type_of g (mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
@@ -1276,6 +1279,7 @@ let invfun qhyp f g =
 			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
 	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
-	  )
+	  end)
 	  qhyp
+          end
 	  g
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a77968092..76095cb1c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -383,7 +383,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
     tclTHENSEQ 
       [
 	h_intros (List.rev rev_ids);
-	intro_using teq_id;
+	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
 	  tclTHENSEQ[
 	    thin to_intros;
@@ -534,15 +534,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
       tclTHENLIST[
-	split (ImplicitBindings [s_max]);
-	intro_then
+	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
+	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
+            Proofview.V82.tactic begin
 	    observe_tac (str "destruct_bounds_aux") 
-	      (tclTHENS (simplest_case (mkVar id))
+	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
 		 [
-		   tclTHENLIST[intro_using h_id;
-			       simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
-			       default_full_auto];
+		   tclTHENLIST[Proofview.V82.of_tactic (intro_using h_id);
+			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
+			       Proofview.V82.of_tactic default_full_auto];
 		   tclTHENLIST[
 		     observe_tac (str "clearing k ") (clear [id]);
 		     h_intros [k;h';def];
@@ -564,25 +565,25 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 			 
 			 (observe_tac (str "finishing") 
 			    (tclORELSE
-			       h_reflexivity
+			       (Proofview.V82.of_tactic h_reflexivity)
 			       (observe_tac (str "calling prove_lt") (prove_lt hyple))))])
 		   ]
 	      ]
-	      ))
+	      )end))
 	  ] g
       | (_,v_bound)::l -> 
       tclTHENLIST[
-	simplest_elim (mkVar v_bound);
+	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
 	h_clear false [v_bound];
-	tclDO 2 intro;
+	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
 	  (fun p_hyp -> 
 	    (onNthHypId 2 
 	       (fun p ->  
 		 tclTHENLIST[
-		   simplest_elim 
-		     (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
-		   tclDO 3 intro;
+		   Proofview.V82.of_tactic (simplest_elim 
+		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
+		   tclDO 3 (Proofview.V82.of_tactic intro);
 		   onNLastHypsId 3 (fun lids -> 
 		     match lids with
 		       [hle2;hle1;pmax] -> 
@@ -606,7 +607,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
       tclTHENLIST[
 	continuation_tac infos;
 	observe_tac (str "first split") 
-	  (split (ImplicitBindings [infos.info]));
+	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
 	observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
@@ -617,7 +618,7 @@ let terminate_others _ expr_info continuation_tac infos =
     tclTHENLIST[
 	    continuation_tac infos;
       observe_tac (str "first split") 
-	(split (ImplicitBindings [infos.info]));
+	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
       observe_tac (str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
@@ -665,7 +666,7 @@ let mkDestructEq :
       (fun g2 ->
 	change_in_concl None
 	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
-      simplest_case expr], to_revert
+      Proofview.V82.of_tactic (simplest_case expr)], to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -711,7 +712,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	then
 	  tclTHENLIST[ 
 	    observe_tac (str "first split")
-	      (split (ImplicitBindings [new_infos.info]));
+	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 	    observe_tac (str "destruct_bounds (3)")
 	      (destruct_bounds new_infos)
 	  ]
@@ -720,11 +721,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
       ]    
     with Not_found -> 
       observe_tac (str "terminate_app_rec not found") (tclTHENS
-	(simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))
+	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
 	[		
 	  tclTHENLIST[
-	    intro_using rec_res_id;
-	    intro;
+	    Proofview.V82.of_tactic (intro_using rec_res_id);
+	    Proofview.V82.of_tactic intro;
 	    onNthHypId 1 
 	      (fun v_bound -> 
 		(onNthHypId 2 
@@ -741,7 +742,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 		       then
 			 tclTHENLIST[ 
 			   observe_tac (str "first split") 
-			     (split (ImplicitBindings [new_infos.info]));
+			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 			   observe_tac (str "destruct_bounds (2)") 
 			     (destruct_bounds new_infos)
 			 ]
@@ -836,12 +837,12 @@ let rec make_rewrite_list expr_info max = function
 	    let def_na,_,_ = destProd t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
-	  general_rewrite_bindings false Locus.AllOccurrences
+	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
 			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S max)]) false g) )
+			      (f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        tclTHENLIST[ (* x < S max proof *)
@@ -863,12 +864,12 @@ let make_rewrite expr_info l hp max =
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
 	 observe_tac (str "general_rewrite_bindings")
-	   (general_rewrite_bindings false Locus.AllOccurrences
+	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
 			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S (f_S max))]) false) g)
+			      (f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (tclTHENLIST[
@@ -879,7 +880,7 @@ let make_rewrite expr_info l hp max =
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
-	   (observe_tac (str "h_reflexivity") h_reflexivity)]))
+	   (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic h_reflexivity))]))
        ;
 	 tclTHENLIST[ (* x < S (S max) proof *)
 	 apply (delayed_force le_lt_SS);
@@ -893,9 +894,9 @@ let rec compute_max rew_tac max l =
     | [] -> rew_tac max
     | (_,p,_)::l -> 
       tclTHENLIST[
-	simplest_elim 
-	  (mkApp(delayed_force max_constr, [| max; mkVar p|]));
-	tclDO 3 intro;
+	Proofview.V82.of_tactic (simplest_elim 
+	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
+	tclDO 3 (Proofview.V82.of_tactic intro);
 	onNLastHypsId 3 (fun lids -> 
 	  match lids with
 	    | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l 
@@ -913,9 +914,9 @@ let rec destruct_hex expr_info acc l =
       end
     | (v,hex)::l -> 
       tclTHENLIST[
-	simplest_case (mkVar hex);
+	Proofview.V82.of_tactic (simplest_case (mkVar hex));
 	clear [hex];
-	tclDO 2 intro;
+	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
 	  onNthHypId 2 (fun p -> 
 	    observe_tac 
@@ -928,7 +929,7 @@ let rec destruct_hex expr_info acc l =
 let rec intros_values_eq expr_info acc = 
   tclORELSE(
     tclTHENLIST[
-      tclDO 2 intro;
+      tclDO 2 (Proofview.V82.of_tactic intro);
       onNthHypId 1 (fun hex -> 
 	(onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
       )
@@ -960,13 +961,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info =
       if expr_info.is_final && expr_info.is_main_branch 
       then 
 	tclTHENLIST
-	  [ simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
 	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
 	  ]
       else 
 	tclTHENLIST[
-  	  simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+  	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
 	]
   end
@@ -1049,22 +1050,22 @@ let termination_proof_header is_mes input_type ids args_id relation
 	(tclTHENS
 	   (observe_tac
 	      (str "first assert")
-	      (assert_tac
+	      (Proofview.V82.of_tactic (assert_tac
 		 (Name wf_rec_arg)
 		 (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
 		 )
-	      )
+	      ))
 	   )
 	   [
 	     (* accesibility proof *)
 	     tclTHENS
 	       (observe_tac
 		  (str "second assert")
-		  (assert_tac
+		  (Proofview.V82.of_tactic (assert_tac
 		     (Name wf_thm)
 		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
-		  )
+		  ))
 	       )
 	       [
 		 (* interactive proof that the relation is well_founded *)
@@ -1086,7 +1087,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       ;
 		observe_tac (str "h_fix") (h_fix (Some hrec) (nargs+1));
 		h_intros args_id;
-		h_intro wf_rec_arg;
+		Proofview.V82.of_tactic (h_intro wf_rec_arg);
 		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
 	       ]
 	   ]
@@ -1271,11 +1272,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	   tclTHENSEQ
 	     [
 	       h_generalize [lemma];
-	       h_intro hid;
+	       Proofview.V82.of_tactic (h_intro hid);
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
 		  tclTHEN
-		    (Elim.h_decompose_and (mkVar hid))
+		    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
 		       lid := List.rev (List.subtract Id.equal ids' ids);
@@ -1288,7 +1289,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       (fun g ->
 	 match kind_of_term (pf_concl g) with
 	   | App(f,_) when eq_constr f (well_founded ()) ->
-	       Auto.h_auto None [] (Some [])  g
+	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
 	       incr h_num;
 	       (observe_tac (str "finishing using")
@@ -1318,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     hook;
   if Indfun_common.is_strict_tcc  ()
   then
-    by (tclIDTAC)
+    by (Proofview.V82.tactic (tclIDTAC))
   else 
     begin
-      by (
+      by (Proofview.V82.tactic begin
 	fun g ->
 	  tclTHEN
 	    (decompose_and_tac)
@@ -1330,17 +1331,17 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	 	  (List.map
 	 	     (fun c ->
 	 		tclTHENSEQ
-	 		  [intros;
+	 		  [Proofview.V82.of_tactic intros;
 	 		   h_simplest_apply (interp_constr Evd.empty (Global.env()) c);
-	 		   tclCOMPLETE Auto.default_auto
+	 		   tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
 	 		  ]
 	 	     )
 	 	     using_lemmas)
 	       ) tclIDTAC)
-	    g)
+	    g end)
     end;
   try
-    by tclIDTAC; (* raises UserError _ if the proof is complete *)
+    by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *)
   with UserError _ ->
     defined ()
 
@@ -1363,9 +1364,9 @@ let com_terminate
       (Global, Proof Lemma) (Environ.named_context_val env)
       (compute_terminate_type nb_args fonctional_ref) hook;
 
-    by (observe_tac (str "starting_tac") tac_start);
-    by (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
-    				   input_type relation rec_arg_num ))
+    by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start));
+    by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+    				   input_type relation rec_arg_num )))
   in
   start_proof tclIDTAC tclIDTAC;
   try
@@ -1391,8 +1392,8 @@ let start_equation (f:global_reference) (term_f:global_reference)
     h_intros x;
     unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
     observe_tac (str "simplest_case")
-      (simplest_case (mkApp (terminate_constr,
-                             Array.of_list (List.map mkVar x))));
+      (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
+                             Array.of_list (List.map mkVar x)))));
     observe_tac (str "prove_eq") (cont_tactic x)] g;;
 
 let (com_eqn : int -> Id.t ->
@@ -1410,7 +1411,7 @@ let (com_eqn : int -> Id.t ->
     (start_proof eq_name (Global, Proof Lemma)
        (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      by
-       (start_equation f_ref terminate_ref
+       (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
 	       {nb_arg=nb_arg;
@@ -1436,7 +1437,7 @@ let (com_eqn : int -> Id.t ->
 		ih = Id.of_string "______";
 	       }
 	  )
-       ); 
+       )); 
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
      Flags.silently (fun () -> Lemmas.save_named opacity) () ; 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index a17c62eba..78d1e1756 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -24,52 +24,52 @@ let out_arg = function
   | ArgArg x -> x
 
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ]
-| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ]
+| [ "psatz_Z" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (out_arg i)) ]
+| [ "psatz_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (-1)) ]
 END
 
 TACTIC EXTEND ZOmicron
-[ "xlia"  ] -> [ Coq_micromega.xlia]
+[ "xlia"  ] -> [  Proofview.V82.tactic (Coq_micromega.xlia) ]
 END
 
 TACTIC EXTEND Nlia
-[ "xnlia"  ] -> [ Coq_micromega.xnlia]
+[ "xnlia"  ] -> [  Proofview.V82.tactic (Coq_micromega.xnlia) ]
 END
 
 
 
 TACTIC EXTEND Sos_Z
-| [ "sos_Z" ] -> [ Coq_micromega.sos_Z]
+| [ "sos_Z" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_Z) ]
    END
 
 TACTIC EXTEND Sos_Q
-| [ "sos_Q" ] -> [ Coq_micromega.sos_Q]
+| [ "sos_Q" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_Q) ]
    END
 
 TACTIC EXTEND Sos_R
-| [ "sos_R" ] -> [ Coq_micromega.sos_R]
+| [ "sos_R" ] -> [  Proofview.V82.tactic (Coq_micromega.sos_R) ]
 END
 
 
 TACTIC EXTEND Omicron
-[ "psatzl_Z"  ] -> [ Coq_micromega.psatzl_Z]
+[ "psatzl_Z"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_Z) ]
 END
 
 TACTIC EXTEND QOmicron
-[ "psatzl_Q"  ] -> [ Coq_micromega.psatzl_Q]
+[ "psatzl_Q"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_Q) ]
 END
 
 TACTIC EXTEND ROmicron
-[ "psatzl_R"  ] -> [ Coq_micromega.psatzl_R]
+[ "psatzl_R"  ] -> [  Proofview.V82.tactic (Coq_micromega.psatzl_R) ]
 END
 
 TACTIC EXTEND RMicromega
-| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ]
-| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ]
+| [ "psatz_R" int_or_var(i) ] -> [  Proofview.V82.tactic (Coq_micromega.psatz_R (out_arg i)) ]
+| [ "psatz_R" ] -> [  Proofview.V82.tactic (Coq_micromega.psatz_R (-1)) ]
 END
 
 TACTIC EXTEND QMicromega
-| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ]
-| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ]
+| [ "psatz_Q" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (out_arg i)) ]
+| [ "psatz_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (-1)) ]
 END
 
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 286fa6335..6fd8ab8e9 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -590,7 +590,7 @@ let nsatz_compute t =
   return_term lpol
 
 TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ nsatz_compute lt ]
+| [ "nsatz_compute"  constr(lt) ] -> [ Proofview.V82.tactic (nsatz_compute lt) ]
 END
 
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4f96d7209..512e372bb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -27,13 +27,16 @@ open Globnames
 open Nametab
 open Contradiction
 open Misctypes
+open Proofview.Notations
 
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
 
-let elim_id id gl = simplest_elim (pf_global gl id) gl
+let elim_id id =
+  Tacmach.New.pf_global id >>- fun c ->
+  simplest_elim c
 let resolve_id id gl = apply (pf_global gl id) gl
 
 let timing timer_name f arg = f arg
@@ -76,13 +79,6 @@ let _ =
       optwrite = write old_style_flag }
 
 
-let all_time        = timing "Omega     "
-let solver_time     = timing "Solver    "
-let exact_time      = timing "Rewrites  "
-let elim_time       = timing "Elim      "
-let simpl_time      = timing "Simpl     "
-let generalize_time = timing "Generalize"
-
 let new_identifier =
   let cpt = ref 0 in
   (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
@@ -124,9 +120,9 @@ let mk_then = tclTHENLIST
 
 let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
-let generalize_tac t = generalize_time (generalize t)
-let elim t = elim_time (simplest_elim t)
-let exact t = exact_time (Tactics.refine t)
+let generalize_tac t = generalize t
+let elim t = simplest_elim t
+let exact t = Tactics.refine t
 let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 
 let rev_assoc k =
@@ -536,7 +532,7 @@ let focused_simpl path gl =
   let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   convert_concl_no_check newc DEFAULTcast gl
 
-let focused_simpl path = simpl_time (focused_simpl path)
+let focused_simpl path = focused_simpl path
 
 type oformula =
   | Oplus of oformula * oformula
@@ -1015,12 +1011,12 @@ let replay_history tactic_normalisation =
   let aux1 = Id.of_string "auxiliary_1" in
   let aux2 = Id.of_string "auxiliary_2" in
   let izero = mk_integer zero in
-  let rec loop t =
+  let rec loop t : unit Proofview.tactic =
     match t with
       | HYP e :: l ->
 	  begin
 	    try
-	      tclTHEN
+	      Tacticals.New.tclTHEN
 		(Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
 		(loop l)
 	    with Not_found -> loop l end
@@ -1032,16 +1028,16 @@ let replay_history tactic_normalisation =
 	  let k = if b then negone else one in
 	  let p_initial = [P_APP 1;P_TYPE] in
 	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
-	  tclTHENLIST [
-	    (generalize_tac
+	  Tacticals.New.tclTHENLIST [
+	    Proofview.V82.tactic (generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
 		mkVar id1; mkVar id2 |])]);
-	    (mk_then tac);
+	    Proofview.V82.tactic (mk_then tac);
 	    (intros_using [aux]);
-	    (resolve_id aux);
+	    Proofview.V82.tactic (resolve_id aux);
             reflexivity
           ]
       | CONTRADICTION (e1,e2) :: l ->
@@ -1055,13 +1051,13 @@ let replay_history tactic_normalisation =
 					Lazy.force coq_Gt;
 					Lazy.force coq_Gt |])
 	    in
-            tclTHENS
-	      (tclTHENLIST [
-		(unfold sp_Zle);
-		(simpl_in_concl);
+            Tacticals.New.tclTHENS
+	      (Tacticals.New.tclTHENLIST [
+		Proofview.V82.tactic (unfold sp_Zle);
+		Proofview.V82.tactic (simpl_in_concl);
 		intro;
 		(absurd not_sup_sup) ])
-	      [ assumption ; reflexivity ]
+	      [ Proofview.V82.tactic assumption ; reflexivity ]
 	  in
 	  let theorem =
             mkApp (Lazy.force coq_OMEGA2, [|
@@ -1069,7 +1065,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le)
+	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (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)
@@ -1079,34 +1075,34 @@ let replay_history tactic_normalisation =
 	  let rhs = mk_plus (mk_times eq2 kk) dd in
 	  let state_eg = mk_eq eq1 rhs in
 	  let tac = scalar_norm_add [P_APP 3] e2.body in
-	  tclTHENS
-	    (cut state_eg)
-	    [ tclTHENS
-	        (tclTHENLIST [
+	  Tacticals.New.tclTHENS
+	    (Proofview.V82.tactic (cut state_eg))
+	    [ Tacticals.New.tclTHENS
+	        (Tacticals.New.tclTHENLIST [
 		  (intros_using [aux]);
-		  (generalize_tac
+		  Proofview.V82.tactic (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
 		      [| eq1; rhs; mkVar aux; mkVar id |])]);
-		  (clear [aux;id]);
+		  Proofview.V82.tactic (clear [aux;id]);
 		  (intros_using [id]);
-		  (cut (mk_gt kk dd)) ])
-	        [ tclTHENS
-		    (cut (mk_gt kk izero))
-		    [ tclTHENLIST [
+		  Proofview.V82.tactic (cut (mk_gt kk dd)) ])
+	        [ Tacticals.New.tclTHENS
+		    (Proofview.V82.tactic (cut (mk_gt kk izero)))
+		    [ Tacticals.New.tclTHENLIST [
 		        (intros_using [aux1; aux2]);
-		        (generalize_tac
+		        (Proofview.V82.tactic (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
-			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
-		        (clear [aux1;aux2;id]);
+			    [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]));
+		        Proofview.V82.tactic (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
-		      tclTHENLIST [
-			(unfold sp_Zgt);
-			(simpl_in_concl);
+		      Tacticals.New.tclTHENLIST [
+			(Proofview.V82.tactic (unfold sp_Zgt));
+			(Proofview.V82.tactic simpl_in_concl);
 			reflexivity ] ];
-		  tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ]
+		  Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ]
                 ];
-	      tclTHEN (mk_then tac) reflexivity ]
+	      Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
 
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
 	  let c = floor_div e1.constant k in
@@ -1117,27 +1113,27 @@ let replay_history tactic_normalisation =
 	  let kk = mk_integer k
 	  and dd = mk_integer d in
 	  let tac = scalar_norm_add [P_APP 2] e2.body in
-	  tclTHENS
-	    (cut (mk_gt dd izero))
-	    [ tclTHENS (cut (mk_gt kk dd))
-		[tclTHENLIST [
+	  Tacticals.New.tclTHENS
+	    (Proofview.V82.tactic (cut (mk_gt dd izero)))
+	    [ Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk dd)))
+		[Tacticals.New.tclTHENLIST [
 		  (intros_using [aux2;aux1]);
-		  (generalize_tac
+		  Proofview.V82.tactic (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
                       [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
-		  (clear [aux1;aux2]);
-		  (unfold sp_not);
+		  Proofview.V82.tactic (clear [aux1;aux2]);
+		  Proofview.V82.tactic (unfold sp_not);
 		  (intros_using [aux]);
-		  (resolve_id aux);
-		  (mk_then tac);
-		  assumption ] ;
-		 tclTHENLIST [
-		   (unfold sp_Zgt);
-		   simpl_in_concl;
+		  Proofview.V82.tactic (resolve_id aux);
+		  Proofview.V82.tactic (mk_then tac);
+		  Proofview.V82.tactic assumption ] ;
+		 Tacticals.New.tclTHENLIST [
+		   Proofview.V82.tactic (unfold sp_Zgt);
+		   Proofview.V82.tactic simpl_in_concl;
 		   reflexivity ] ];
-              tclTHENLIST [
-		(unfold sp_Zgt);
-                simpl_in_concl;
+              Tacticals.New.tclTHENLIST [
+		Proofview.V82.tactic (unfold sp_Zgt);
+                Proofview.V82.tactic simpl_in_concl;
 		reflexivity ] ]
       | EXACT_DIVIDE (e1,k) :: l ->
 	  let id = hyp_of_tag e1.id in
@@ -1148,36 +1144,36 @@ let replay_history tactic_normalisation =
 	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
 	  if e1.kind == DISE then
             let tac = scalar_norm [P_APP 3] e2.body in
-            tclTHENS
-	      (cut state_eq)
-	      [tclTHENLIST [
+            Tacticals.New.tclTHENS
+	      (Proofview.V82.tactic (cut state_eq))
+	      [Tacticals.New.tclTHENLIST [
 		(intros_using [aux1]);
-		(generalize_tac
+		Proofview.V82.tactic (generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
                     [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
-		(clear [aux1;id]);
+		Proofview.V82.tactic (clear [aux1;id]);
 		(intros_using [id]);
 		(loop l) ];
-	       tclTHEN (mk_then tac) reflexivity ]
+	       Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
 	  else
             let tac = scalar_norm [P_APP 3] e2.body in
-            tclTHENS (cut state_eq)
+            Tacticals.New.tclTHENS (Proofview.V82.tactic (cut state_eq))
 	      [
-		tclTHENS
-		 (cut (mk_gt kk izero))
-		 [tclTHENLIST [
+		Tacticals.New.tclTHENS
+		 (Proofview.V82.tactic (cut (mk_gt kk izero)))
+		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   (generalize_tac
+		   Proofview.V82.tactic (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
 		       [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
-		   (clear [aux1;aux2;id]);
+		   Proofview.V82.tactic (clear [aux1;aux2;id]);
 		   (intros_using [id]);
 		   (loop l) ];
-		  tclTHENLIST [
-		    (unfold sp_Zgt);
-                    simpl_in_concl;
+		  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (unfold sp_Zgt);
+                    Proofview.V82.tactic simpl_in_concl;
 		    reflexivity ] ];
-		tclTHEN (mk_then tac) reflexivity ]
+		Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
       | (MERGE_EQ(e3,e1,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1190,16 +1186,16 @@ let replay_history tactic_normalisation =
 	      (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
             scalar_norm [P_APP 3] e1.body
 	  in
-	  tclTHENS
-	    (cut (mk_eq eq1 (mk_inv eq2)))
-	    [tclTHENLIST [
+	  Tacticals.New.tclTHENS
+	    (Proofview.V82.tactic (cut (mk_eq eq1 (mk_inv eq2))))
+	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
-	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
+	      Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
-	      (clear [id1;id2;aux]);
+	      Proofview.V82.tactic (clear [id1;id2;aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            tclTHEN (mk_then tac) reflexivity]
+            Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
 
       | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
 	  let id = new_identifier ()
@@ -1223,21 +1219,21 @@ let replay_history tactic_normalisation =
               [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
             shuffle_mult_right p_initial
               orig.body m ({c= negone;v= v}::def.body) in
-	  tclTHENS
-	    (cut theorem)
-	    [tclTHENLIST [
+	  Tacticals.New.tclTHENS
+	    (Proofview.V82.tactic (cut theorem))
+	    [Tacticals.New.tclTHENLIST [
 	      (intros_using [aux]);
 	      (elim_id aux);
-	      (clear [aux]);
+	      Proofview.V82.tactic (clear [aux]);
 	      (intros_using [vid; aux]);
-	      (generalize_tac
+	      Proofview.V82.tactic (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
-	      (mk_then tac);
-	      (clear [aux]);
+	      Proofview.V82.tactic (mk_then tac);
+	      Proofview.V82.tactic (clear [aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            tclTHEN (exists_tac eq1) reflexivity ]
+            Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
       | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
 	  let id1 = new_identifier ()
 	  and id2 = new_identifier () in
@@ -1246,10 +1242,10 @@ let replay_history tactic_normalisation =
 	  let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
 	  let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
 	  let eq = val_of(decompile e) in
-	  tclTHENS
+	  Tacticals.New.tclTHENS
 	    (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
-	    [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ];
-             tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+	    [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ];
+             Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]]
       | SUM(e3,(k1,e1),(k2,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1268,10 +1264,10 @@ let replay_history tactic_normalisation =
             let p_initial =
               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
-            tclTHENLIST [
-	      (generalize_tac
+            Tacticals.New.tclTHENLIST [
+	      Proofview.V82.tactic (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
-	      (mk_then tac);
+	      Proofview.V82.tactic (mk_then tac);
 	      (intros_using [id]);
 	      (loop l)
             ]
@@ -1280,43 +1276,43 @@ let replay_history tactic_normalisation =
 	    and kk2 = mk_integer k2 in
 	    let p_initial = [P_APP 2;P_TYPE] in
 	    let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
-            tclTHENS (cut (mk_gt kk1 izero))
-	      [tclTHENS
-		 (cut (mk_gt kk2 izero))
-		 [tclTHENLIST [
+            Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk1 izero)))
+	      [Tacticals.New.tclTHENS
+		 (Proofview.V82.tactic (cut (mk_gt kk2 izero)))
+		 [Tacticals.New.tclTHENLIST [
 		   (intros_using [aux2;aux1]);
-		   (generalize_tac
+		   Proofview.V82.tactic (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
 		       eq1;eq2;kk1;kk2;
 		       mkVar aux1;mkVar aux2;
 		       mkVar id1;mkVar id2 |])]);
-		   (clear [aux1;aux2]);
-		   (mk_then tac);
+		   Proofview.V82.tactic (clear [aux1;aux2]);
+		   Proofview.V82.tactic (mk_then tac);
 		   (intros_using [id]);
 		   (loop l) ];
-		 tclTHENLIST [
-		   (unfold sp_Zgt);
-                   simpl_in_concl;
+		 Tacticals.New.tclTHENLIST [
+		   Proofview.V82.tactic (unfold sp_Zgt);
+                   Proofview.V82.tactic simpl_in_concl;
 		   reflexivity ] ];
-	      tclTHENLIST [
-		(unfold sp_Zgt);
-                simpl_in_concl;
+	      Tacticals.New.tclTHENLIST [
+		Proofview.V82.tactic (unfold sp_Zgt);
+                Proofview.V82.tactic simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl
+	  Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
-	  tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
+	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
-	  tclTHENLIST [
-	    (generalize_tac [mkVar (hyp_of_tag e)]);
-            (unfold sp_Zle);
-	    simpl_in_concl;
-	    (unfold sp_not);
+	  Tacticals.New.tclTHENLIST [
+	    Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
+            Proofview.V82.tactic (unfold sp_Zle);
+	    Proofview.V82.tactic simpl_in_concl;
+	    Proofview.V82.tactic (unfold sp_not);
 	    (intros_using [aux]);
-	    (resolve_id aux);
+	    Proofview.V82.tactic (resolve_id aux);
 	    reflexivity
           ]
-      | _ -> tclIDTAC
+      | _ -> Proofview.tclUNIT ()
   in
   loop
 
@@ -1336,7 +1332,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   in
   if not (List.is_empty tac) then
     let id' = new_identifier () in
-    ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ]))
+    ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ]))
           :: tactic,
      compile id' flag t' :: defs)
   else
@@ -1377,12 +1373,18 @@ let destructure_omega gl tac_def (id,c) =
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
-  tclTHEN (tclTRY (clear [id])) (intro_using id)
+  Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id)
+
+
+open Proofview.Notations
 
-let coq_omega gl =
+let coq_omega =
+  Proofview.tclUNIT () >= fun () -> (* delay for the effects in [clear_tables] *)
   clear_tables ();
+  Tacmach.New.pf_hyps_types >>- fun hyps_types ->
+  Tacmach.New.of_old destructure_omega >>- fun destructure_omega ->
   let tactic_normalisation, system =
-    List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in
+    List.fold_left destructure_omega ([],[]) hyps_types in
   let prelude,sys =
     List.fold_left
       (fun (tac,sys) (t,(v,th,b)) ->
@@ -1390,78 +1392,79 @@ let coq_omega gl =
            let id = new_identifier () in
            let i = new_id () in
            tag_hypothesis id i;
-           (tclTHENLIST [
+           (Tacticals.New.tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
 	     (intros_using [v; id]);
 	     (elim_id id);
-	     (clear [id]);
+	     Proofview.V82.tactic (clear [id]);
 	     (intros_using [th;id]);
 	     tac ]),
            {kind = INEQ;
 	    body = [{v=intern_id v; c=one}];
             constant = zero; id = i} :: sys
 	 else
-           (tclTHENLIST [
+           (Tacticals.New.tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_new_var, [t])));
 	     (intros_using [v;th]);
 	     tac ]),
            sys)
-      (tclIDTAC,[]) (dump_tables ())
+      (Proofview.tclUNIT (),[]) (dump_tables ())
   in
   let system = system @ sys in
   if !display_system_flag then display_system display_var system;
   if !old_style_flag then begin
     try
       let _ = simplify (new_id,new_var_num,display_var) false system in
-      tclIDTAC gl
+      Proofview.tclUNIT ()
     with UNSOLVABLE ->
       let _,path = depend [] [] (history ()) in
       if !display_action_flag then display_action display_var path;
-      (tclTHEN prelude (replay_history tactic_normalisation path)) gl
+      (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path))
   end else begin
     try
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
-      (tclTHEN prelude (replay_history tactic_normalisation path)) gl
-    with NO_CONTRADICTION -> error "Omega can't solve this system"
+      Tacticals.New.(tclTHEN prelude (replay_history tactic_normalisation path))
+    with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
   end
 
-let coq_omega = solver_time coq_omega
+let coq_omega = coq_omega
 
-let nat_inject gl =
-  let rec explore p t =
+let nat_inject =
+  Tacmach.New.pf_apply Reductionops.is_conv >>- fun is_conv ->
+  let rec explore p t : unit Proofview.tactic =
     try match destructurate_term t with
       | Kapp(Plus,[t1;t2]) ->
-          tclTHENLIST [
-	    (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+          Tacticals.New.tclTHENLIST [
+	    Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_plus),[t1;t2]));
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
       | Kapp(Mult,[t1;t2]) ->
-          tclTHENLIST [
-	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+          Tacticals.New.tclTHENLIST [
+	    Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_mult),[t1;t2]));
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
       | Kapp(Minus,[t1;t2]) ->
           let id = new_identifier () in
-          tclTHENS
-            (tclTHEN
+          Tacticals.New.tclTHENS
+            (Tacticals.New.tclTHEN
 	       (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
 	       (intros_using [id]))
 	    [
-	      tclTHENLIST [
-	        (clever_rewrite_gen p
+	      Tacticals.New.tclTHENLIST [
+	        Proofview.V82.tactic (clever_rewrite_gen p
 		  (mk_minus (mk_inj t1) (mk_inj t2))
                   ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
 		(loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
 		(explore (P_APP 1 :: p) t1);
 		(explore (P_APP 2 :: p) t2) ];
-	      (tclTHEN
-		 (clever_rewrite_gen p (mk_integer zero)
-                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
+	      (Tacticals.New.tclTHEN
+		 (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero)
+                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])))
 		 (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
 	    ]
       | Kapp(S,[t']) ->
@@ -1472,37 +1475,37 @@ let nat_inject gl =
               | _ -> false
             with e when catchable_exception e -> false
 	  in
-          let rec loop p t =
+          let rec loop p t : unit Proofview.tactic =
             try match destructurate_term t with
 		Kapp(S,[t]) ->
-                  (tclTHEN
-                     (clever_rewrite_gen p
+                  (Tacticals.New.tclTHEN
+                     (Proofview.V82.tactic (clever_rewrite_gen p
 			(mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
-			((Lazy.force coq_inj_S),[t]))
+			((Lazy.force coq_inj_S),[t])))
 		     (loop (P_APP 1 :: p) t))
               | _ -> explore p t
             with e when catchable_exception e -> explore p t
 	  in
-          if is_number t' then focused_simpl p else loop p t
+          if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t
       | Kapp(Pred,[t]) ->
           let t_minus_one =
 	    mkApp (Lazy.force coq_minus, [| t;
 		      mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
-          tclTHEN
-            (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
-               ((Lazy.force coq_pred_of_minus),[t]))
+          Tacticals.New.tclTHEN
+            (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
+               ((Lazy.force coq_pred_of_minus),[t])))
             (explore p t_minus_one)
-      | Kapp(O,[]) -> focused_simpl p
-      | _ -> tclIDTAC
-    with e when catchable_exception e -> tclIDTAC
+      | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p)
+      | _ -> Proofview.tclUNIT ()
+    with e when catchable_exception e -> Proofview.tclUNIT ()
 
   and loop = function
-    | [] -> tclIDTAC
+    | [] -> Proofview.tclUNIT ()
     | (i,t)::lit ->
 	  begin try match destructurate_prop t with
               Kapp(Le,[t1;t2]) ->
-		tclTHENLIST [
-		  (generalize_tac
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (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);
@@ -1510,8 +1513,8 @@ let nat_inject gl =
 		  (loop lit)
                 ]
             | Kapp(Lt,[t1;t2]) ->
-		tclTHENLIST [
-		  (generalize_tac
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (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);
@@ -1519,8 +1522,8 @@ let nat_inject gl =
 		  (loop lit)
                 ]
             | Kapp(Ge,[t1;t2]) ->
-		tclTHENLIST [
-		  (generalize_tac
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (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);
@@ -1528,8 +1531,8 @@ let nat_inject gl =
 		  (loop lit)
                 ]
             | Kapp(Gt,[t1;t2]) ->
-		tclTHENLIST [
-		  (generalize_tac
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (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);
@@ -1537,8 +1540,8 @@ let nat_inject gl =
 		  (loop lit)
                 ]
             | Kapp(Neq,[t1;t2]) ->
-		tclTHENLIST [
-		  (generalize_tac
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (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);
@@ -1546,9 +1549,9 @@ let nat_inject gl =
 		  (loop lit)
                 ]
             | Kapp(Eq,[typ;t1;t2]) ->
-		if pf_conv_x gl typ (Lazy.force coq_nat) then
-                  tclTHENLIST [
-		    (generalize_tac
+		if is_conv typ (Lazy.force coq_nat) then
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (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);
@@ -1559,7 +1562,8 @@ let nat_inject gl =
 	    | _ -> loop lit
 	  with e when catchable_exception e -> loop lit end
   in
-  loop (List.rev (pf_hyps_types gl)) gl
+  Tacmach.New.pf_hyps_types >>- fun hyps_types ->
+  loop (List.rev hyps_types)
 
 let dec_binop = function
   | Zne -> coq_dec_Zne
@@ -1627,50 +1631,51 @@ let rec decidability gl t =
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
-  tclTHEN
-    (tclTRY (clear [id]))
-    (fun gl ->
-      let id = fresh_id [] id gl in
-      tclTHEN (introduction id) (tac id) gl)
+  Tacticals.New.tclTHEN
+    (Proofview.V82.tactic (tclTRY (clear [id])))
+    (Tacmach.New.of_old (fresh_id [] id) >>- fun id ->
+     Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id))
 
 let onClearedName2 id tac =
-  tclTHEN
-    (tclTRY (clear [id]))
-    (fun gl ->
-      let id1 = fresh_id [] (add_suffix id "_left") gl in
-      let id2 = fresh_id [] (add_suffix id "_right") gl in
-      tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] gl)
-
-let destructure_hyps gl =
+  Tacticals.New.tclTHEN
+    (Proofview.V82.tactic (tclTRY (clear [id])))
+    (Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) >>- fun id1 ->
+     Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) >>- fun id2 ->
+      Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ])
+
+let destructure_hyps =
+  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  Tacmach.New.of_old decidability >>- fun decidability ->
+  Tacmach.New.of_old pf_nf >>- fun pf_nf ->
   let rec loop = function
-    | [] -> (tclTHEN nat_inject coq_omega)
+    | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
     | (i,body,t)::lit ->
 	begin try match destructurate_prop t with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
-              (tclTHENS
+              (Tacticals.New.tclTHENS
                 (elim_id i)
                 [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
                   onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
-              tclTHEN
+              Tacticals.New.tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop ((i1,None,t1)::(i2,None,t2)::lit)))
           | Kapp(Iff,[t1;t2]) ->
-	      tclTHEN
+	      Tacticals.New.tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit)))
           | Kimp(t1,t2) ->
 	      (* t1 and t2 might be in Type rather than Prop.
 		 For t1, the decidability check will ensure being Prop. *)
-              if is_Prop (pf_type_of gl t2)
+              if is_Prop (type_of t2)
               then
-		let d1 = decidability gl t1 in
-		tclTHENLIST [
-		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
+		let d1 = decidability t1 in
+		Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                     [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
@@ -1680,26 +1685,26 @@ let destructure_hyps gl =
           | Kapp(Not,[t]) ->
               begin match destructurate_prop t with
 		  Kapp(Or,[t1;t2]) ->
-                    tclTHENLIST [
-		      (generalize_tac
+                    Tacticals.New.tclTHENLIST [
+		      Proofview.V82.tactic (generalize_tac
                         [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
                     ]
 		| Kapp(And,[t1;t2]) ->
-		    let d1 = decidability gl t1 in
-                    tclTHENLIST [
-		      (generalize_tac
+		    let d1 = decidability t1 in
+                    Tacticals.New.tclTHENLIST [
+		      Proofview.V82.tactic (generalize_tac
 		        [mkApp (Lazy.force coq_not_and,
 				[| t1; t2; d1; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
                     ]
 		| Kapp(Iff,[t1;t2]) ->
-		    let d1 = decidability gl t1 in
-		    let d2 = decidability gl t2 in
-                    tclTHENLIST [
-		      (generalize_tac
+		    let d1 = decidability t1 in
+		    let d2 = decidability t2 in
+                    Tacticals.New.tclTHENLIST [
+		      Proofview.V82.tactic (generalize_tac
 		        [mkApp (Lazy.force coq_not_iff,
 				[| t1; t2; d1; d2; mkVar i |])]);
 		      (onClearedName i (fun i ->
@@ -1710,42 +1715,42 @@ let destructure_hyps gl =
 		| Kimp(t1,t2) ->
 		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
 		       For t1, being decidable implies being Prop. *)
-		    let d1 = decidability gl t1 in
-                    tclTHENLIST [
-		      (generalize_tac
+		    let d1 = decidability t1 in
+                    Tacticals.New.tclTHENLIST [
+		      Proofview.V82.tactic (generalize_tac
 		        [mkApp (Lazy.force coq_not_imp,
 				[| t1; t2; d1; mkVar i |])]);
 		      (onClearedName i (fun i ->
                         (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
                     ]
 		| Kapp(Not,[t]) ->
-		    let d = decidability gl t in
-                    tclTHENLIST [
-		      (generalize_tac
+		    let d = decidability t in
+                    Tacticals.New.tclTHENLIST [
+		      Proofview.V82.tactic (generalize_tac
 			[mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		      (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
                     ]
 		| Kapp(op,[t1;t2]) ->
 		    (try
 		      let thm = not_binop op in
-                      tclTHENLIST [
-			(generalize_tac
+                      Tacticals.New.tclTHENLIST [
+			Proofview.V82.tactic (generalize_tac
 			   [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 			(onClearedName i (fun _ -> loop lit))
                       ]
 		     with Not_found -> loop lit)
 		| Kapp(Eq,[typ;t1;t2]) ->
                     if !old_style_flag then begin
-		      match destructurate_type (pf_nf gl typ) with
+		      match destructurate_type (pf_nf typ) with
 			| Kapp(Nat,_) ->
-                            tclTHENLIST [
+                            Tacticals.New.tclTHENLIST [
 			      (simplest_elim
 				(mkApp
                                   (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
 			      (onClearedName i (fun _ -> loop lit))
                             ]
 			| Kapp(Z,_) ->
-                            tclTHENLIST [
+                            Tacticals.New.tclTHENLIST [
 			      (simplest_elim
 				(mkApp
 				  (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
@@ -1753,18 +1758,18 @@ let destructure_hyps gl =
                             ]
 			| _ -> loop lit
                     end else begin
-		      match destructurate_type (pf_nf gl typ) with
+		      match destructurate_type (pf_nf typ) with
 			| Kapp(Nat,_) ->
-                               (tclTHEN
-			       (convert_hyp_no_check
+                               (Tacticals.New.tclTHEN
+			       (Proofview.V82.tactic (convert_hyp_no_check
                                   (i,body,
-				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
 			       (loop lit))
 			| Kapp(Z,_) ->
-                               (tclTHEN
-			       (convert_hyp_no_check
+                               (Tacticals.New.tclTHEN
+			       (Proofview.V82.tactic (convert_hyp_no_check
                                   (i,body,
-				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
 			       (loop lit))
 			| _ -> loop lit
                     end
@@ -1776,37 +1781,37 @@ let destructure_hyps gl =
 	  | e when catchable_exception e -> loop lit
 	end
   in
-  loop (pf_hyps gl) gl
+  Goal.hyps >>- fun hyps ->
+  loop (Environ.named_context_of_val hyps)
 
-let destructure_goal gl =
-  let concl = pf_concl gl in
+let destructure_goal =
+  Goal.concl >>- fun concl ->
+  Tacmach.New.of_old decidability >>- fun decidability ->
   let rec loop t =
     match destructurate_prop t with
       | Kapp(Not,[t]) ->
-          (tclTHEN
-	     (tclTHEN (unfold sp_not) intro)
+          (Tacticals.New.tclTHEN
+	     (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro)
 	     destructure_hyps)
-      | Kimp(a,b) -> (tclTHEN intro (loop b))
+      | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
       | _ ->
 	let goal_tac =
 	  try
-	    let dec = decidability gl t in
-	    tclTHEN
-	      (Tactics.refine
-		 (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))
+	    let dec = decidability t in
+	    Tacticals.New.tclTHEN
+              (Proofview.V82.tactic (Tactics.refine
+		 (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	      intro
-	  with Undecidable -> Tactics.elim_type (build_coq_False ())
+	  with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
 	in
-	tclTHEN goal_tac destructure_hyps
+	Tacticals.New.tclTHEN goal_tac destructure_hyps
   in
-  (loop concl) gl
+  (loop concl)
 
-let destructure_goal = all_time (destructure_goal)
+let destructure_goal = destructure_goal
 
-let omega_solver gl =
+let omega_solver =
+  Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
   Coqlib.check_required_library ["Coq";"omega";"Omega"];
-  let result = destructure_goal gl in
-  (* if !display_time_flag then begin text_time ();
-     flush Pervasives.stdout end; *)
-  result
+  destructure_goal
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 082eac422..0aad364c1 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -28,9 +28,9 @@ let omega_tactic l =
        | s -> Errors.error ("No Omega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
-  tclTHEN
-    (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
-    omega_solver
+  Tacticals.New.tclTHEN
+    (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs))
+    (omega_solver)
 
 
 TACTIC EXTEND omega
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 92b27c3e8..0cf4d3bb4 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -109,6 +109,7 @@ open Pattern
 open Patternops
 open Matching
 open Tacmach
+open Proofview.Notations
 (*i*)
 
 (*s First, we need to access some Coq constants
@@ -219,14 +220,16 @@ let compute_rhs bodyi index_of_f =
 
 (*s Now the function [compute_ivs] itself *)
 
-let compute_ivs gl f cs =
+let compute_ivs f cs =
   let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
-        begin match decomp_term body3 with
+	Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv ->
+        Goal.return
+          begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
               let n_lhs_rhs = ref []
               and v_lhs = ref (None : constr option)
@@ -245,8 +248,7 @@ let compute_ivs gl f cs =
            (* Then we test if the RHS is the RHS for variables *)
                    else begin match decompose_app bodyi with
                      | vmf, [_; _; a3; a4 ]
-                         when isRel a3 && isRel a4 &&
-			   pf_conv_x gl vmf
+                         when isRel a3 && isRel a4 && is_conv vmf
                            (Lazy.force coq_varmap_find)->
                              v_lhs := Some (compute_lhs
                                               (snd (List.hd args3))
@@ -389,7 +391,10 @@ module Constrhash = Hashtbl.Make
   [ivs : inversion_scheme]\\
   [lc: constr list]\\
   [gl: goal sigma]\\ *)
-let quote_terms ivs lc gl =
+let quote_terms ivs lc =
+  (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in
+     [Coqlib.check_required_library]. *)
+  Goal.return () >- fun () ->
   Coqlib.check_required_library ["Coq";"quote";"Quote"];
   let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
@@ -436,36 +441,41 @@ let quote_terms ivs lc gl =
     auxl ivs.normal_lhs_rhs
   in
   let lp = List.map aux lc in
-  (lp, (btree_of_array (Array.of_list (List.rev !varlist))
-          ivs.return_type ))
+  Goal.return begin
+    (lp, (btree_of_array (Array.of_list (List.rev !varlist))
+            ivs.return_type ))
+  end
 
 (*s actually we could "quote" a list of terms instead of a single
   term. Ring for example needs that, but Ring doesn't use Quote
   yet. *)
 
-let quote f lid gl =
-  let f = pf_global gl f in
-  let cl = List.map (pf_global gl) lid in
-  let ivs = compute_ivs gl f cl in
-  let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with
+let quote f lid =
+  Tacmach.New.pf_global f >>- fun f ->
+  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
+  compute_ivs f cl >>- fun ivs ->
+  Goal.concl >>- fun concl ->
+  quote_terms ivs [concl] >>- fun quoted_terms ->
+  let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
-
-let gen_quote cont c f lid gl =
-  let f = pf_global gl f in
-  let cl = List.map (pf_global gl) lid in
-  let ivs = compute_ivs gl f cl in
-  let (p, vm) = match quote_terms ivs [c] gl with
+    | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
+    | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+
+let gen_quote cont c f lid =
+  Tacmach.New.pf_global f >>- fun f ->
+  Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl ->
+  compute_ivs f cl >>- fun ivs ->
+  quote_terms ivs [c] >>- fun quoted_terms ->
+  let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> cont (mkApp (f, [| p |])) gl
-    | Some _ -> cont (mkApp (f, [| vm; p |])) gl
+    | None -> cont (mkApp (f, [| p |]))
+    | Some _ -> cont (mkApp (f, [| vm; p |]))
 
 (*i
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 055546c8b..efe11b99c 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -21,14 +21,14 @@ let romega_tactic l =
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
-  tclTHEN
-    (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
-    (tclTHEN
+  Tacticals.New.tclTHEN
+    (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs)))
+    (Tacticals.New.tclTHEN
        (* because of the contradiction process in (r)omega,
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
-       Tactics.intros
-       total_reflexive_omega_tactic)
+       (Tactics.intros)
+       (Proofview.V82.tactic total_reflexive_omega_tactic))
 
 
 TACTIC EXTEND romega
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index af4e33964..7d0b7a1bc 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -9,6 +9,6 @@
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 TACTIC EXTEND rtauto
-  [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ]
+  [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
 END
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 74ad34eff..907cd474c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -97,9 +97,9 @@ let protect_tac_in map id =
 
 TACTIC EXTEND protect_fv
   [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ protect_tac_in map id ]
+    [ Proofview.V82.tactic (protect_tac_in map id) ]
 | [ "protect_fv" string(map) ] ->
-    [ protect_tac map ]
+    [ Proofview.V82.tactic (protect_tac map) ]
 END;;
 
 (****************************************************************************)
@@ -112,7 +112,7 @@ let closed_term t l =
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term t l ]
+    [ Proofview.V82.tactic (closed_term t l) ]
 END
 ;;
 
@@ -192,7 +192,7 @@ let exec_tactic env n f args =
     Tacexp(TacFun(List.map(fun id -> Some id) lid,
                   Tacintern.glob_tactic(tacticIn get_res))) in
   let _ =
-    Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
+    Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) (dummy_goal env) in
   !res
 
 let constr_of v = match Value.to_constr v with
@@ -795,15 +795,17 @@ let ltac_ring_structure e =
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
-let ring_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
+open Proofview.Notations
+
+let ring_lookup (f:glob_tactic_expr) lH rl t =
+  Goal.env >>- fun env ->
+  Goal.defs >>- fun sigma ->
   let rl = make_args_list rl t in
   let e = find_ring_structure env sigma rl in
   let rl = carg (make_term_list e.ring_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let ring = ltac_ring_structure e in
-  ltac_apply f (ring@[lH;rl]) gl
+  ltac_apply f (ring@[lH;rl])
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
@@ -1116,15 +1118,15 @@ let ltac_field_structure e =
   [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
-let field_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
+let field_lookup (f:glob_tactic_expr) lH rl t =
+  Goal.env >>- fun env ->
+  Goal.defs >>- fun sigma ->
   let rl = make_args_list rl t in
   let e = find_field_structure env sigma rl in
   let rl = carg (make_term_list e.field_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let field = ltac_field_structure e in
-  ltac_apply f (field@[lH;rl]) gl
+  ltac_apply f (field@[lH;rl])
 
 
 TACTIC EXTEND field_lookup