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

2 files changed, 243 insertions, 238 deletions

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