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

9 files changed, 185 insertions, 165 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index ff1dab46af..8e49a5cfaa 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -24,6 +24,7 @@ open Tactics
 open Tacticals
 open Ind_tables
 open Misctypes
+open Proofview.Notations
 
 (**********************************************************************)
 (* Generic synthesis of boolean equality *)
@@ -326,7 +327,7 @@ let destruct_ind c =
 so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
-let do_replace_lb lb_scheme_key aavoid narg gls p q =
+let do_replace_lb lb_scheme_key aavoid narg p q =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -350,35 +351,39 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
         )))
       )
   in
-  let type_of_pq = pf_type_of gls p in
+  Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+  let type_of_pq = type_of p in
     let u,v = destruct_ind type_of_pq
-    in let lb_type_of_p, eff =
-        try 
+    in let lb_type_of_p =
+        try
           let c, eff = find_scheme lb_scheme_key u in
-          mkConst c, eff
+          Proofview.tclUNIT (mkConst c, eff)
         with Not_found ->
           (* spiwack: the format of this error message should probably
 	              be improved. *)
-          let err_msg = string_of_ppcmds
-	                              (str "Leibniz->boolean:" ++
-                                       str "You have to declare the" ++
-				       str "decidability over " ++
-				       Printer.pr_constr type_of_pq ++
-				       str " first.")
+          let err_msg =
+	    (str "Leibniz->boolean:" ++
+             str "You have to declare the" ++
+	     str "decidability over " ++
+	     Printer.pr_constr type_of_pq ++
+	     str " first.")
           in
-          error err_msg
-    in let lb_args = Array.append (Array.append
+          Proofview.tclZERO (Errors.UserError("",err_msg))
+       in
+       lb_type_of_p >= fun (lb_type_of_p,eff) ->
+       let lb_args = Array.append (Array.append
                           (Array.map (fun x -> x) v)
                           (Array.map (fun x -> do_arg x 1) v))
                           (Array.map (fun x -> do_arg x 2) v)
         in let app =  if Array.equal eq_constr lb_args [||]
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
-            in 
-            [Tactics.emit_side_effects eff;
-             Equality.replace p q ; apply app ; Auto.default_auto]
+           in
+           Tacticals.New.tclTHENLIST [
+             Proofview.V82.tactic (Tactics.emit_side_effects eff);
+             Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
 
 (* used in the bool -> leib side *)
-let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -405,14 +410,16 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
 
   let rec aux l1 l2 =
     match (l1,l2) with
-    | (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in
+    | (t1::q1,t2::q2) ->
+        Tacmach.New.pf_apply Typing.type_of >>- fun type_of ->
+        let tt1 = type_of t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
           (* trick so that the good sequence is returned*)
                 with e when Errors.noncritical e -> ind,[||]
           in if eq_ind u ind
-             then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
+             then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
              else (
                let bl_t1, eff =
                try 
@@ -438,30 +445,36 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
                 let app =  if Array.equal eq_constr bl_args [||]
                            then bl_t1 else mkApp (bl_t1,bl_args)
                 in
-                  (Tactics.emit_side_effects eff)::
-                  (Equality.replace_by t1 t2
-                    (tclTHEN (apply app) (Auto.default_auto)))::(aux q1 q2)
+                Tacticals.New.tclTHENLIST [
+                  Proofview.V82.tactic (Tactics.emit_side_effects eff) ;
+                  Equality.replace_by t1 t2
+                    (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply app)) (Auto.default_auto)) ;
+                  aux q1 q2 ]
               )
         )
-    | ([],[]) -> []
-    | _ -> error "Both side of the equality must have the same arity."
-  in
-  let (ind1,ca1) =
-    try destApp lft with DestKO -> error "replace failed."
-  and (ind2,ca2) =
-    try destApp rgt with DestKO -> error "replace failed."
-  in
-  let (sp1,i1) =
-    try destInd ind1 with DestKO ->
-      try fst (destConstruct ind1) with DestKO ->
-        error "The expected type is an inductive one."
-  and (sp2,i2) =
-    try destInd ind2 with DestKO ->
-      try fst (destConstruct ind2)  with DestKO ->
-        error "The expected type is an inductive one."
+    | ([],[]) -> Proofview.tclUNIT ()
+    | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
   in
+  begin try Proofview.tclUNIT (destApp lft)
+    with DestKO ->  Proofview.tclZERO (UserError ("" , str"replace failed."))
+  end >= fun (ind1,ca1) ->
+  begin try Proofview.tclUNIT (destApp rgt)
+    with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
+  end >= fun (ind2,ca2) ->
+  begin try Proofview.tclUNIT (destInd ind1)
+    with DestKO ->
+      begin try Proofview.tclUNIT (fst (destConstruct ind1))
+        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+      end
+  end >= fun (sp1,i1) ->
+  begin try Proofview.tclUNIT (destInd ind2)
+    with DestKO ->
+      begin try Proofview.tclUNIT (fst (destConstruct ind2))
+        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+      end
+  end >= fun (sp2,i2) ->
   if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
-  then error "Eq should be on the same type"
+  then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type"))
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
 (*
@@ -530,7 +543,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|]))
         ))), eff
 
-let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
+let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let avoid = ref [] in
       let first_intros =
@@ -538,67 +551,66 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
         ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @
         ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
       in
-      let fresh_first_intros = List.map ( fun s ->
-        let fresh = fresh_id (!avoid) s gsig in
-        avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
-      let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (Id.of_string "y") gsig in
-      let freshz = avoid := freshm::(!avoid);
-            fresh_id (!avoid) (Id.of_string "Z") gsig in
+      let fresh_id s =
+        Tacmach.New.of_old begin fun gsig ->
+          let fresh = fresh_id (!avoid) s gsig in
+          avoid := fresh::(!avoid); fresh
+        end
+      in
+      Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+      fresh_id (Id.of_string "x") >>- fun freshn ->
+      fresh_id (Id.of_string "y") >>- fun freshm ->
+      fresh_id (Id.of_string "Z") >>- fun freshz ->
   (* try with *)
-      avoid := freshz::(!avoid);
-      tclTHENSEQ [ intros_using fresh_first_intros;
+      Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      induct_on (mkVar freshn);
                      intro_using freshm;
                      destruct_on (mkVar freshm);
                      intro_using freshz;
                      intros;
-                     tclTRY (
-                      tclORELSE reflexivity (Equality.discr_tac false None)
+                     Tacticals.New.tclTRY (
+                      Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     simpl_in_hyp (freshz,Locus.InHyp);
+                     Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp));
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
-                    tclREPEAT (
-                      tclTHENSEQ [
+                    Tacticals.New.tclREPEAT (
+                      Tacticals.New.tclTHENLIST [
                          simple_apply_in freshz (andb_prop());
-                         fun gl ->
-                           let fresht = fresh_id (!avoid) (Id.of_string "Z") gsig
-                           in
-                            avoid := fresht::(!avoid);
+                           fresh_id (Id.of_string "Z") >>- fun fresht ->
                             (new_destruct false [Tacexpr.ElimOnConstr
                                       (Evd.empty,((mkVar freshz,NoBindings)))]
                                   None
                                   (None, Some (dl,IntroOrAndPattern [[
                                     dl,IntroIdentifier fresht;
-                                    dl,IntroIdentifier freshz]])) None) gl
+                                    dl,IntroIdentifier freshz]])) None)
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn
  replace bi with ai; auto || replace bi with ai by  apply typeofbi_prod ; auto
 *)
-                    fun gls-> let gl = pf_concl gls in
+                      Goal.concl >>- fun gl ->
                       match (kind_of_term gl) with
                       | App (c,ca) -> (
                         match (kind_of_term c) with
                         | Ind indeq ->
                             if eq_gr (IndRef indeq) Coqlib.glob_eq
-                            then (
-                              tclTHENSEQ ((do_replace_bl bl_scheme_key ind gls
-				                      (!avoid)
-                                                      nparrec (ca.(2))
-                              (ca.(1)))@[Auto.default_auto]) gls
-                            )
+                            then
+                              Tacticals.New.tclTHEN
+                                (do_replace_bl bl_scheme_key ind
+				   (!avoid)
+                                   nparrec (ca.(2))
+                                   (ca.(1)))
+                                Auto.default_auto
                             else
-                              (error "Failure while solving Boolean->Leibniz.")
-                        | _ -> error "Failure while solving Boolean->Leibniz."
+                              Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
+                        | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
                       )
-                      | _ -> error "Failure while solving Boolean->Leibniz."
+                      | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
 
-                    ] gsig
+                    ]
 
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -661,7 +673,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
         ))), eff
 
-let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
+let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
@@ -669,49 +681,50 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
         ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
         ( List.map (fun (_,_,_,slb) -> slb) list_id )
       in
-      let fresh_first_intros = List.map ( fun s ->
-        let fresh = fresh_id (!avoid) s gsig in
-        avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
-      let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (Id.of_string "y") gsig in
-      let freshz = avoid := freshm::(!avoid);
-            fresh_id (!avoid) (Id.of_string "Z") gsig in
+      let fresh_id s =
+        Tacmach.New.of_old begin fun gsig ->
+          let fresh = fresh_id (!avoid) s gsig in
+          avoid := fresh::(!avoid); fresh
+        end
+      in
+      Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+      fresh_id (Id.of_string "x") >>- fun freshn ->
+      fresh_id (Id.of_string "y") >>- fun freshm ->
+      fresh_id (Id.of_string "Z") >>- fun freshz ->
   (* try with *)
-      avoid := freshz::(!avoid);
-      tclTHENSEQ [ intros_using fresh_first_intros;
+      Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
                      intro_using freshn ;
                      induct_on (mkVar freshn);
                      intro_using freshm;
                      destruct_on (mkVar freshm);
                      intro_using freshz;
                      intros;
-                     tclTRY (
-                      tclORELSE reflexivity (Equality.discr_tac false None)
+                     Tacticals.New.tclTRY (
+                      Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
                      Equality.inj None false (mkVar freshz,NoBindings);
-		     intros; simpl_in_concl;
+		     intros; (Proofview.V82.tactic simpl_in_concl);
                      Auto.default_auto;
-                     tclREPEAT (
-                      tclTHENSEQ [apply (andb_true_intro());
+                     Tacticals.New.tclREPEAT (
+                      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
                                   simplest_split ;Auto.default_auto ]
                       );
-                      fun gls -> let gl = pf_concl gls in
+                      Goal.concl >>- fun gl ->
                   (* assume the goal to be eq (eq_type ...) = true *)
                         match (kind_of_term gl) with
                           | App(c,ca) -> (match (kind_of_term ca.(1)) with
                               | App(c',ca') ->
                                   let n = Array.length ca' in
-                                    tclTHENSEQ (do_replace_lb lb_scheme_key
-				                (!avoid)
-                                                nparrec gls
-                                                ca'.(n-2) ca'.(n-1)) gls
-                              | _ -> error
-                                "Failure while solving Leibniz->Boolean."
+                                    do_replace_lb lb_scheme_key
+				    (!avoid)
+                                    nparrec
+                                    ca'.(n-2) ca'.(n-1)
+                              | _ ->
+                                Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
                             )
-                          | _ -> error
-                                  "Failure while solving Leibniz->Boolean."
-                    ] gsig
+                          | _ ->
+                              Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                    ]
 
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
@@ -793,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
         )
       )
 
-let compute_dec_tact ind lnamesparrec nparrec gsig =
+let compute_dec_tact ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eqI, eff = eqI ind lnamesparrec in
   let avoid = ref [] in
@@ -805,64 +818,65 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
       ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
       ( List.map (fun (_,_,_,slb) -> slb) list_id )
   in
-  let fresh_first_intros = List.map ( fun s ->
-    let fresh = fresh_id (!avoid) s gsig in
-    avoid := fresh::(!avoid); fresh ) first_intros in
-  let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
-  let freshm = avoid := freshn::(!avoid);
-    fresh_id (!avoid) (Id.of_string "y") gsig in
-  let freshH = avoid := freshm::(!avoid);
-    fresh_id (!avoid) (Id.of_string "H") gsig in
+  let fresh_id s =
+    Tacmach.New.of_old begin fun gsig ->
+      let fresh = fresh_id (!avoid) s gsig in
+      avoid := fresh::(!avoid); fresh
+    end
+  in
+  Goal.sensitive_list_map fresh_id first_intros >>- fun fresh_first_intros ->
+  fresh_id (Id.of_string "x") >>- fun freshn ->
+  fresh_id (Id.of_string "y") >>- fun freshm ->
+  fresh_id (Id.of_string "H") >>- fun freshH ->
   let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
-  avoid := freshH::(!avoid);
   let arfresh = Array.of_list fresh_first_intros in
   let xargs = Array.sub arfresh 0 (2*nparrec) in
-  let blI, eff' = 
-    try let c, eff = find_scheme bl_scheme_kind ind in mkConst c, eff with
-            Not_found -> error (
-              "Error during the decidability part, boolean to leibniz"^
-              " equality is required.")
-  in
-  let lbI, eff'' =
-    try let c, eff = find_scheme lb_scheme_kind ind in mkConst c, eff with
-            Not_found -> error (
-              "Error during the decidability part, leibniz to boolean"^
-              " equality is required.")
-  in
-  tclTHENSEQ [
-        Tactics.emit_side_effects
+  begin try
+          let c, eff = find_scheme bl_scheme_kind ind in
+          Proofview.tclUNIT (mkConst c,eff) with
+    Not_found ->
+      Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++
+        str" equality is required."))
+  end >= fun (blI,eff') ->
+  begin try
+          let c, eff = find_scheme lb_scheme_kind ind in
+          Proofview.tclUNIT (mkConst c,eff) with
+    Not_found ->
+      Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
+        str" equality is required."))
+  end >= fun (lbI,eff'') ->
+  Tacticals.New.tclTHENLIST [
+        Proofview.V82.tactic (Tactics.emit_side_effects
           (Declareops.union_side_effects eff''
-            (Declareops.union_side_effects eff' eff));
+            (Declareops.union_side_effects eff' eff)));
         intros_using fresh_first_intros;
         intros_using [freshn;freshm];
 	(*we do this so we don't have to prove the same goal twice *)
         assert_by (Name freshH) (
           mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
 	)
-	  (tclTHEN (destruct_on eqbnm) Auto.default_auto);
-        (fun gsig ->
-	  let freshH2 = fresh_id (!avoid) (Id.of_string "H") gsig in
-          avoid := freshH2::(!avoid);
-	  tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
+	  (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
+
+          fresh_id (Id.of_string "H") >>- fun freshH2 ->
+	  Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
 	    (* left *)
-	    tclTHENSEQ [
+	    Tacticals.New.tclTHENLIST [
 	      simplest_left;
-              apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
+              Proofview.V82.tactic (apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)));
               Auto.default_auto
             ];
+
 	    (*right *)
-            (fun gsig ->
-	    let freshH3 = fresh_id (!avoid) (Id.of_string "H") gsig in
-            avoid := freshH3::(!avoid);
-            tclTHENSEQ [
+            fresh_id (Id.of_string "H") >>- fun freshH3 ->
+            Tacticals.New.tclTHENLIST [
 	      simplest_right ;
-              unfold_constr (Lazy.force Coqlib.coq_not_ref);
+              Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref));
               intro;
-              Equality.subst_all;
+              Equality.subst_all ?flags:None;
               assert_by (Name freshH3)
 		(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
-		(tclTHENSEQ [
-		  apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
+		(Tacticals.New.tclTHENLIST [
+		  Proofview.V82.tactic (apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)));
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true
@@ -873,9 +887,9 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
                               )
                               true;
               Equality.discr_tac false None
-	    ] gsig)
-	  ] gsig)
-  ] gsig
+	    ]
+	  ]
+  ]
 
 let make_eq_decidability mind =
   let mib = Global.lookup_mind mind in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2648f8e362..121f8f4e1a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -117,7 +117,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
 
 let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
     ?(generalize=true)
-    ?(tac:Proof_type.tactic option) ?hook pri =
+    ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let tclass, ids =
@@ -301,7 +301,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		if not (Option.is_empty term) then 
 		  Pfedit.by (!refine_ref (evm, Option.get term))
 		else if Flags.is_auto_intros () then
-		  Pfedit.by (Refiner.tclDO len Tactics.intro);
+		  Pfedit.by (Tacticals.New.tclDO len Tactics.intro);
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	       id)
 	end)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 5a0dc97c24..a8e611928e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -53,7 +53,7 @@ val new_instance :
   typeclass_constraint ->
   constr_expr option ->
   ?generalize:bool ->
-  ?tac:Proof_type.tactic  ->
+  ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
   int option ->
   Id.t
@@ -74,4 +74,4 @@ val context : local_binder list -> bool
 
 (** Forward ref for refine *)
 
-val refine_ref : (open_constr -> Proof_type.tactic) ref
+val refine_ref : (open_constr -> unit Proofview.tactic) ref
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e63ff19915..0a2f9c3c39 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -830,6 +830,9 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
+    let init_tac =
+      Option.map (List.map Proofview.V82.tactic) init_tac
+    in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
       (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
   else begin
@@ -857,6 +860,9 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
+    let init_tac =
+      Option.map (List.map Proofview.V82.tactic) init_tac
+    in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
       (Some(true,[],init_tac)) thms None (fun _ _ -> ())
   else begin
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index d6b868b004..91886e076e 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -313,22 +313,22 @@ let rec_tac_initializer finite guard thms snl =
 
 let start_proof_with_initialization kind recguard thms snl hook =
   let intro_tac (_, (_, (ids, _))) =
-    Refiner.tclMAP (function
+    Tacticals.New.tclMAP (function
     | Name id -> Tactics.intro_mustbe_force id
     | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = rec_tac_initializer finite guard thms snl in
+      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then 
-              tclTHENS rec_tac (List.map intro_tac thms)
+              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
             else
               rec_tac
         | Some tacl ->
-            tclTHENS rec_tac
+            Tacticals.New.tclTHENS rec_tac
             (if Flags.is_auto_intros () then
-              List.map2 (fun tac thm -> tclTHEN tac (intro_tac thm)) tacl thms
+              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
             else
               tacl)),guard
   | None ->
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index e8998d6089..25e5a44304 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -19,7 +19,7 @@ open Pfedit
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : Id.t -> goal_kind -> types ->
-  ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
 val start_proof_com : goal_kind ->
@@ -27,7 +27,7 @@ val start_proof_com : goal_kind ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> (bool * lemma_possible_guards * tactic list option) option ->
+  goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 15e197a983..13e12b7e15 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -53,7 +53,7 @@ type oblinfo =
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
     ev_typ: types;
-    ev_tac: tactic option;
+    ev_tac: unit Proofview.tactic option;
     ev_deps: Int.Set.t }
 
 (* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
@@ -302,7 +302,7 @@ let explain_no_obligations = function
 
 type obligation_info =
     (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
-     Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
+     Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
 
 type obligation =
   { obl_name : Id.t;
@@ -311,7 +311,7 @@ type obligation =
     obl_body : constr option;
     obl_status : Evar_kinds.obligation_definition_status;
     obl_deps : Int.Set.t;
-    obl_tac : tactic option;
+    obl_tac : unit Proofview.tactic option;
   }
 
 type obligations = (obligation array * int)
@@ -762,7 +762,7 @@ let rec string_of_list sep f = function
 let solve_by_tac evi t =
   let id = Id.of_string "H" in
   let entry = Pfedit.build_constant_by_tactic 
-    id ~goal_kind evi.evar_hyps evi.evar_concl (tclCOMPLETE t) in
+    id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Term_typing.handle_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index df9b53df5d..feebf94ec4 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -41,7 +41,7 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
 val eterm_obligations : env -> Id.t -> evar_map -> int ->
   ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
   (Id.t * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t *
-      tactic option) array
+      unit Proofview.tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
@@ -53,7 +53,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
 
 type obligation_info =
   (Id.t * Term.types * Evar_kinds.t Loc.located *
-      Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
+      Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
@@ -63,7 +63,7 @@ type progress = (* Resolution status of a program *)
   | Defined of global_reference (* Defined as id *)
       
 val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * Proof_type.tactic
+val get_default_tactic : unit -> locality_flag * unit Proofview.tactic
 val print_default_tactic : unit -> Pp.std_ppcmds
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
@@ -72,7 +72,7 @@ val get_proofs_transparency : unit -> bool
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
-  ?tactic:Proof_type.tactic ->
+  ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
   ?hook:unit Tacexpr.declaration_hook -> obligation_info -> progress
 
@@ -86,7 +86,7 @@ type fixpoint_kind =
 val add_mutual_definitions :
   (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
-  ?tactic:Proof_type.tactic ->
+  ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
   ?hook:unit Tacexpr.declaration_hook ->
@@ -98,14 +98,14 @@ val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
 
 val next_obligation : Names.Id.t option -> Tacexpr.raw_tactic_expr option -> unit
 
-val solve_obligations : Names.Id.t option -> Proof_type.tactic option -> progress
+val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
 
-val solve_all_obligations : Proof_type.tactic option -> unit
+val solve_all_obligations : unit Proofview.tactic option -> unit
 
-val try_solve_obligation : int -> Names.Id.t option -> Proof_type.tactic option -> unit
+val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
 
-val try_solve_obligations : Names.Id.t option -> Proof_type.tactic option -> unit
+val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
 
 val show_obligations : ?msg:bool -> Names.Id.t option -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9ee91815e9..a0a355a154 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -475,7 +475,7 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  by (Tactics.exact_proof c);
+  by (Tactics.New.exact_proof c);
   save_named true
 
 let vernac_assumption locality (local, kind) l nl =