Merge PR#568: Remove tactic compatibility layer

39 files changed, 757 insertions, 653 deletions

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index bb193ebb55..fad6472911 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,7 +25,7 @@ echo $TRAVIS_PULL_REQUEST
 echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
-if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then
-    mathcomp_CI_BRANCH=no_camlp4_compat
-    mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
+if [ $TRAVIS_PULL_REQUEST == "568" ] || [ $TRAVIS_BRANCH == "remove-tactic-compat" ]; then
+    fiat_parsers_CI_BRANCH=fix-ml
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat.git
 fi
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7f915b7819..8ea1638c99 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,15 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+** Tactic API **
+
+- pf_constr_of_global now returns a tactic instead of taking a continuation.
+  Thus it only generates one instance of the global reference, and it is the
+  caller's responsibility to perform a focus on the goal.
+
+- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
+  was very specific. Use tclPROGRESS instead.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2d9dec095a..00b31cccee 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -239,21 +239,43 @@ let build_projection intype (cstr:pconstructor) special default gls=
 
 (* generate an adhoc tactic following the proof tree  *)
 
-let _M =mkMeta
-
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-
-let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-
-let new_refine c = Proofview.V82.tactic (refine c)
-let refine c = refine c
+  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
+
+let rec gen_holes env sigma t n accu =
+  let open Sigma in
+  if Int.equal n 0 then (sigma, List.rev accu)
+  else match EConstr.kind sigma t with
+  | Prod (_, u, t) ->
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in
+    let sigma = Sigma.to_evar_map sigma in
+    let t = EConstr.Vars.subst1 ev t in
+    gen_holes env sigma t (pred n) (ev :: accu)
+  | _ -> assert false
+
+let app_global_with_holes f args n =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    Refine.refine { Sigma.run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
+      let t = Tacmach.New.pf_get_type_of gl fc in
+      let t = Termops.prod_applist sigma t (Array.to_list args) in
+      let ans = mkApp (fc, args) in
+      let (sigma, holes) = gen_holes env sigma t n [] in
+      let ans = applist (ans, holes) in
+      let evdref = ref sigma in
+      let () = Typing.e_check env evdref ans concl in
+      Sigma.Unsafe.of_pair (ans, !evdref)
+    end }
+  end }
 
 let assert_before n c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
-      Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
+    Sigma.Unsafe.of_pair (assert_before n c, evm)
   end }
 
 let refresh_type env evm ty =
@@ -281,18 +303,18 @@ let rec proof_tac p : unit Proofview.tactic =
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
 	refresh_universes (type_of l) (fun typ ->
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
+        app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
 	refresh_universes (type_of lr) (fun typ ->
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
+        app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | 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
 	refresh_universes (type_of t2) (fun typ ->
-	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
+	let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
+          Tacticals.New.tclTHENS 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
@@ -303,18 +325,18 @@ let rec proof_tac p : unit Proofview.tactic =
 	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
+	let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
 	let prf =
-	  app_global _trans_eq
+	  app_global_with_holes _trans_eq
 		[|typfx;
 		  mkApp(tf1,[|tx1|]);
 		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|]);_M 2;_M 3|] in
-	  Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine))
-	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1);
+		  mkApp(tf2,[|tx2|])|] 2 in
+	  Tacticals.New.tclTHENS prf
+	    [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
   	     Tacticals.New.tclFIRST
-	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
+	       [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
@@ -330,8 +352,8 @@ let rec proof_tac p : unit Proofview.tactic =
            build_projection intype cstr special default gl
          in
 	 let injt=
-           app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
+           app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
+	   Tacticals.New.tclTHEN injt (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
@@ -341,27 +363,29 @@ let refute_tac c t1 t2 p =
   let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
   let k intype =
-    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
+    let neweq= app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
-let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl c in
-    Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
+let refine_exact_check c =
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+    Sigma.Unsafe.of_pair (exact_check c, evm)
+  end }
 
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
-    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let neweq= app_global _eq [|sort;tt1;tt2|] in
     let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
     let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity=mkLambda (Name x,sort,mkRel 1) in
-    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+    let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+			   [proof_tac p; endt refine_exact_check]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
@@ -392,27 +416,25 @@ let discriminate_tac (cstr,u as cstru) p =
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
     let proj = build_projection intype cstru trivial concl gl in
-    let injt=app_global _f_equal
+    let injt = app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
             app_global _eq_rect
 		       [|outtype;trivial;pred;identity;concl;injt|] k) in
-    let neweq=new_app_global _eq [|intype;t1;t2|] in
+    let neweq = app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+      [proof_tac p; endt refine_exact_check])
   end }
 
 (* wrap everything *)
 
-let build_term_to_complete uf meta pac =
+let build_term_to_complete uf pac =
   let cinfo = get_constructor_info uf pac.cnode in
-  let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
-  let dummy_args = List.rev (List.init pac.arity meta) in
-  let all_args = List.rev_append real_args dummy_args in
+  let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in
   let (kn, u) = cinfo.ci_constr in
-    applist (mkConstructU (kn, EInstance.make u), all_args)
+  (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -434,16 +456,17 @@ let cc_tactic depth additionnal_terms =
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
+            let open Glob_term in
             let env = Proofview.Goal.env gl in
-	    let metacnt = ref 0 in
-	    let newmeta _ = incr metacnt; _M !metacnt in
-	    let terms_to_complete =
-	      List.map
-		(build_term_to_complete uf newmeta)
-		(epsilons uf) in
+            let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+            let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+            let pr_missing (c, missing) =
+              let c = Detyping.detype ~lax:true false [] env sigma c in
+              let holes = List.init missing (fun _ -> hole) in
+              Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes))
+            in
 	    Feedback.msg_info
-	      (Pp.str "Goal is solvable by congruence but \
- some arguments are missing.");
+	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");
 	    Feedback.msg_info
 	      (Pp.str "  Try " ++
 		 hov 8
@@ -451,7 +474,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (Termops.print_constr_env env sigma)
+		     pr_missing
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
@@ -472,13 +495,13 @@ let cc_tactic depth additionnal_terms =
 		convert_to_hyp_tac ida ta idb tb p
   end }
 
-let cc_fail gls =
-  user_err ~hdr:"Congruence" (Pp.str "congruence failed.")
+let cc_fail =
+  Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
   Tacticals.New.tclORELSE
     (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
-    (Proofview.V82.tactic cc_fail)
+    cc_fail
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
    might be slow now, let's rather do something equivalent
@@ -492,16 +515,15 @@ let congruence_tac depth l =
 *)
 
 let mk_eq f c1 c2 k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-			  (k term)
-    end })
+    Sigma.Unsafe.of_pair (k term, evm)
+    end }
 
 let f_equal =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -511,7 +533,7 @@ let f_equal =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
 	  (mk_eq _eq c1 c2 Tactics.cut)
-	  [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)]
+	  [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index de6eb982ee..5099d847b0 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -14,7 +14,7 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
 val cc_tactic : int -> constr list ->  unit Proofview.tactic
 
-val cc_fail : tactic
+val cc_fail : unit Proofview.tactic
 
 val congruence_tac : int -> constr list -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7773f6a2fd..ade94e98e3 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -9,6 +9,7 @@
 open Hipattern
 open Names
 open Term
+open EConstr
 open Vars
 open Termops
 open Tacmach
@@ -44,28 +45,27 @@ let rec nb_prod_after n c=
 	1+(nb_prod_after 0 b)
     | _ -> 0
 
-let construct_nhyps ind gls =
+let construct_nhyps env ind =
   let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
-  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let constr_types = Inductiveops.arities_of_constructors env ind in
   let hyp = nb_prod_after nparams in
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
-let ind_hyps nevar ind largs gls=
-  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
+let ind_hyps env sigma nevar ind largs =
+  let types= Inductiveops.arities_of_constructors env ind in
   let myhyps t =
-    let t1=Term.prod_applist t largs in
-    let t2=snd (decompose_prod_n_assum nevar t1) in
-      fst (decompose_prod_assum t2) in
+    let t = EConstr.of_constr t in
+    let t1=Termops.prod_applist sigma t largs in
+    let t2=snd (decompose_prod_n_assum sigma nevar t1) in
+      fst (decompose_prod_assum sigma t2) in
     Array.map myhyps types
 
-let special_nf gl=
-  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> CClosure.norm_val infos (CClosure.inject t))
+let special_nf env sigma t =
+  Reductionops.clos_norm_flags !red_flags env sigma t
 
-let special_whd gl=
-  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let special_whd env sigma t =
+  Reductionops.clos_whd_flags !red_flags env sigma t
 
 type kind_of_formula=
     Arrow of constr*constr
@@ -78,20 +78,19 @@ type kind_of_formula=
 
 let pop t = Vars.lift (-1) t
 
-let kind_of_formula gl term =
-  let normalize=special_nf gl in
-  let cciterm=special_whd gl term in
-    match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
-	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b)))
+let kind_of_formula env sigma term =
+  let normalize = special_nf env sigma in
+  let cciterm = special_whd env sigma term in
+    match match_with_imp_term sigma cciterm with
+	Some (a,b)-> Arrow (a, pop b)
       |_->
-	 match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
-	     Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
+	 match match_with_forall_term sigma cciterm with
+	     Some (_,a,b)-> Forall (a, b)
 	   |_->
-	      match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with
+	      match match_with_nodep_ind sigma cciterm with
 		  Some (i,l,n)->
-                    let l = List.map EConstr.Unsafe.to_constr l in
-		    let ind,u=EConstr.destInd (project gl) i in
-		    let u = EConstr.EInstance.kind (project gl) u in
+		    let ind,u=EConstr.destInd sigma i in
+		    let u = EConstr.EInstance.kind sigma u in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -100,7 +99,7 @@ let kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
+			    Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
@@ -112,11 +111,11 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
+		    match match_with_sigma_type sigma cciterm with
 			Some (i,l)->
-                          let (ind, u) = EConstr.destInd (project gl) i in
-                          let u = EConstr.EInstance.kind (project gl) u in
-                          Exists((ind, u), List.map EConstr.Unsafe.to_constr l)
+                          let (ind, u) = EConstr.destInd sigma i in
+                          let u = EConstr.EInstance.kind sigma u in
+                          Exists((ind, u), l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
@@ -127,29 +126,29 @@ let no_atoms = (false,{positive=[];negative=[]})
 
 let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
-let build_atoms gl metagen side cciterm =
+let build_atoms env sigma metagen side cciterm =
   let trivial =ref false
   and positive=ref []
   and negative=ref [] in
-  let normalize=special_nf gl in
-  let rec build_rec env polarity cciterm=
-    match kind_of_formula gl cciterm with
+  let normalize=special_nf env sigma in
+  let rec build_rec subst polarity cciterm=
+    match kind_of_formula env sigma cciterm with
 	False(_,_)->if not polarity then trivial:=true
       | Arrow (a,b)->
-	  build_rec env (not polarity) a;
-	  build_rec env polarity b
+	  build_rec subst (not polarity) a;
+	  build_rec subst polarity b
       | And(i,l,b) | Or(i,l,b)->
 	  if b then
 	    begin
-	      let unsigned=normalize (substnl env 0 cciterm) in
+	      let unsigned=normalize (substnl subst 0 cciterm) in
 		if polarity then
 		  positive:= unsigned :: !positive
 		else
 		  negative:= unsigned :: !negative
 	    end;
-	  let v = ind_hyps 0 i l gl in
+	  let v = ind_hyps env sigma 0 i l in
 	  let g i _ decl =
-	    build_rec env polarity (lift i (RelDecl.get_type decl)) in
+	    build_rec subst polarity (lift i (RelDecl.get_type decl)) in
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
@@ -158,16 +157,16 @@ let build_atoms gl metagen side cciterm =
 	    Array.iter f v
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
-	  let v =(ind_hyps 1 i l gl).(0) in
+	  let v =(ind_hyps env sigma 1 i l).(0) in
 	  let g i _ decl =
-	    build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in
+	    build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
-	    build_rec (var::env) polarity b
+	    build_rec (var::subst) polarity b
       | Atom t->
-	  let unsigned=substnl env 0 t in
-	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
+	  let unsigned=substnl subst 0 t in
+	    if not (isMeta sigma unsigned) then (* discarding wildcard atoms *)
 	      if polarity then
 		positive:= unsigned :: !positive
 	      else
@@ -177,9 +176,9 @@ let build_atoms gl metagen side cciterm =
 	  Concl    -> build_rec [] true cciterm
 	| Hyp      -> build_rec [] false cciterm
 	| Hint     ->
-	    let rels,head=decompose_prod cciterm in
-	    let env=List.rev_map (fun _->mkMeta (metagen true)) rels in
-	      build_rec env false head;trivial:=false (* special for hints *)
+	    let rels,head=decompose_prod sigma cciterm in
+	    let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
+	      build_rec subst false head;trivial:=false (* special for hints *)
     end;
     (!trivial,
      {positive= !positive;
@@ -215,32 +214,32 @@ type t={id:global_reference;
 	pat:(left_pattern,right_pattern) sum;
 	atoms:atoms}
 
-let build_formula side nam typ gl metagen=
-  let normalize = special_nf gl in
+let build_formula env sigma side nam typ metagen=
+  let normalize = special_nf env sigma in
     try
       let m=meta_succ(metagen false) in
       let trivial,atoms=
 	if !qflag then
-	  build_atoms gl metagen side typ
+	  build_atoms env sigma metagen side typ
 	else no_atoms in
       let pattern=
 	match side with
 	    Concl ->
 	      let pat=
-		match kind_of_formula gl typ with
+		match kind_of_formula env sigma typ with
 		    False(_,_)        -> Rfalse
 		  | Atom a       -> raise (Is_atom a)
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in
+		      let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
 		Right pat
 	  | _ ->
 	      let pat=
-		match kind_of_formula gl typ with
+		match kind_of_formula env sigma typ with
 		    False(i,_)        ->  Lfalse
 		  | Atom a       ->  raise (Is_atom a)
 		  | And(i,_,b)         ->
@@ -257,7 +256,7 @@ let build_formula side nam typ gl metagen=
 		  | Arrow (a,b) ->
 		      let nfa=normalize a in
 			LA (nfa,
-			    match kind_of_formula gl a with
+			    match kind_of_formula env sigma a with
 				False(i,l)-> LLfalse(i,l)
 			      | Atom t->     LLatom
 			      | And(i,l,_)-> LLand(i,l)
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 5db8ff59ad..3f438c04a0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Globnames
 
 val qflag : bool ref
@@ -23,10 +24,10 @@ type ('a,'b) sum = Left of 'a | Right of 'b
 
 type counter = bool -> metavariable
 
-val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
+val construct_nhyps : Environ.env -> pinductive -> int array
 
-val ind_hyps : int -> pinductive -> constr list ->
-  Proof_type.goal Tacmach.sigma -> Context.Rel.t array
+val ind_hyps : Environ.env -> Evd.evar_map -> int -> pinductive ->
+  constr list -> EConstr.rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
 
@@ -34,7 +35,7 @@ type side = Hyp | Concl | Hint
 
 val dummy_id: global_reference
 
-val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
+val build_atoms : Environ.env -> Evd.evar_map -> counter ->
   side -> constr -> bool * atoms
 
 type right_pattern =
@@ -69,6 +70,6 @@ type t={id: global_reference;
 
 (*exception Is_atom of constr*)
 
-val build_formula : side -> global_reference -> types ->
-  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
+val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types ->
+  counter -> (t,types) sum
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3c03193196..8ef6a09d0e 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -13,7 +13,9 @@ open Formula
 open Sequent
 open Ground
 open Goptions
-open Tacticals
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
 open Tacinterp
 open Libnames
 open Stdarg
@@ -81,21 +83,29 @@ END
 
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 
-let gen_ground_tac flag taco ids bases gl=
+let gen_ground_tac flag taco ids bases =
   let backup= !qflag in
-    try
+  Proofview.tclOR begin
+  Proofview.Goal.enter { enter = begin fun gl ->
       qflag:=flag;
       let solver=
 	match taco with
 	    Some tac-> tac
 	  | None-> snd (default_solver ()) in
-      let startseq gl=
+      let startseq k =
+        Proofview.Goal.s_enter { s_enter = begin fun gl ->
 	let seq=empty_seq !ground_depth in
-        let seq,gl = extend_with_ref_list ids seq gl in
-        extend_with_auto_hints bases seq gl in
-      let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
-	qflag:=backup;result
-    with reraise -> qflag:=backup;raise reraise
+        let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
+        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
+        Sigma.Unsafe.of_pair (k seq, sigma)
+        end }
+      in
+      let result=ground_tac solver startseq in
+      qflag := backup;
+      result
+  end }
+  end
+  (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
 
 (* special for compatibility with Intuition
 
@@ -144,18 +154,15 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
+      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
+      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ]
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
+      [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
+     [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
 END
-
-open Proofview.Notations
-open Cc_plugin
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d6cd7e2a08..ab1dd07c11 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,8 +12,9 @@ open Sequent
 open Rules
 open Instances
 open Term
-open Tacmach
-open Tacticals
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
@@ -29,18 +30,24 @@ let update_flags ()=
       CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
-let ground_tac solver startseq gl=
+let ground_tac solver startseq =
+  Proofview.Goal.enter { enter = begin fun gl ->
   update_flags ();
-  let rec toptac skipped seq gl=
-    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Feedback.msg_debug (Printer.pr_goal gl);
+  let rec toptac skipped seq =
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let () =
+      if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
+      then
+        let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in
+        Feedback.msg_debug (Printer.pr_goal gl)
+    in
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
-	  let (hd,seq1)=take_formula seq
-	  and re_add s=re_add_formula_list skipped s in
+	  let (hd,seq1)=take_formula (project gl) seq
+	  and re_add s=re_add_formula_list (project gl) skipped s in
 	  let continue=toptac []
-	  and backtrack gl=toptac (hd::skipped) seq1 gl in
+	  and backtrack =toptac (hd::skipped) seq1 in
 	    match hd.pat with
 		Right rpat->
 		  begin
@@ -60,7 +67,7 @@ let ground_tac solver startseq gl=
 			  or_tac  backtrack continue (re_add seq1)
 		      | Rfalse->backtrack
 		      | Rexists(i,dom,triv)->
-			  let (lfp,seq2)=collect_quantified seq in
+			  let (lfp,seq2)=collect_quantified (project gl) seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    if  !qflag && seq.depth>0 then
 			      quantified_tac lfp backtrack2
@@ -80,7 +87,7 @@ let ground_tac solver startseq gl=
 			  left_or_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lforall (_,_,_)->
-			  let (lfp,seq2)=collect_quantified seq in
+			  let (lfp,seq2)=collect_quantified (project gl) seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    if  !qflag && seq.depth>0 then
 			      quantified_tac lfp backtrack2
@@ -119,7 +126,8 @@ let ground_tac solver startseq gl=
 			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
 		  end
 	    with Heap.EmptyHeap->solver
-      end gl in
-    let seq, gl' = startseq gl in
-    wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
-
+      end
+    end } in
+    let n = List.length (Proofview.Goal.hyps gl) in
+    startseq (fun seq -> wrap n true (toptac []) seq)
+  end }
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index b5669463cd..4fd1e38a27 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -6,6 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val ground_tac:     Tacmach.tactic ->
-  (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic
+val ground_tac: unit Proofview.tactic ->
+  ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 9dc2a51a61..62f811546d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -11,10 +11,12 @@ open Rules
 open CErrors
 open Util
 open Term
+open EConstr
 open Vars
-open Tacmach
+open Tacmach.New
 open Tactics
-open Tacticals
+open Tacticals.New
+open Proofview.Notations
 open Termops
 open Reductionops
 open Formula
@@ -25,11 +27,12 @@ open Sigma.Notations
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
+        let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
 	match inst1,inst2 with
 	    Phantom(d1),Phantom(d2)->
-	      (OrderedConstr.compare d1 d2)
+	      (cmp d1 d2)
 	  | Real((m1,c1),n1),Real((m2,c2),n2)->
-	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
+	      ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
 	  | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
 	  | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
 
@@ -56,12 +59,12 @@ let make_simple_atoms seq=
       | None->[]
   in {negative=seq.latoms;positive=ratoms}
 
-let do_sequent setref triv id seq i dom atoms=
+let do_sequent sigma setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
     let do_pair t1 t2 =
-      match unif_atoms i dom t1 t2 with
+      match unif_atoms sigma i dom t1 t2 with
 	  None->()
 	| Some (Phantom _) ->phref:=true
 	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
@@ -71,26 +74,26 @@ let do_sequent setref triv id seq i dom atoms=
     do_atoms atoms (make_simple_atoms seq);
     !flag && !phref
 
-let match_one_quantified_hyp setref seq lf=
+let match_one_quantified_hyp sigma setref seq lf=
   match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-	if do_sequent setref triv lf.id seq i dom lf.atoms then
+	if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
 	  setref:=IS.add ((Phantom dom),lf.id) !setref
     | _ -> anomaly (Pp.str "can't happen")
 
-let give_instances lf seq=
+let give_instances sigma lf seq=
   let setref=ref IS.empty in
-    List.iter (match_one_quantified_hyp setref seq) lf;
+    List.iter (match_one_quantified_hyp sigma setref seq) lf;
     IS.elements !setref
 
 (* collector for the engine *)
 
-let rec collect_quantified seq=
+let rec collect_quantified sigma seq=
   try
-    let hd,seq1=take_formula seq in
+    let hd,seq1=take_formula sigma seq in
       (match hd.pat with
 	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
-	     let (q,seq2)=collect_quantified seq1 in
+	     let (q,seq2)=collect_quantified sigma seq1 in
 	       ((hd::q),seq2)
 	 | _->[],seq)
   with Heap.EmptyHeap -> [],seq
@@ -99,60 +102,61 @@ let rec collect_quantified seq=
 
 let dummy_bvid=Id.of_string "x"
 
-let mk_open_instance id idc gl m t=
-  let env=pf_env gl in
-  let evmap=Refiner.project gl in
+let mk_open_instance env evmap id idc m t =
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl idc in
+      let typ=Typing.unsafe_type_of env evmap idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
+      let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
-      let nid=(fresh_id avoid var_id gl) in
+      let nid=(fresh_id_in_env avoid var_id env) in
       let evmap = Sigma.Unsafe.of_evar_map evmap in
       let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let evmap = Sigma.to_evar_map evmap in
       let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
-    evmap, decls, revt
+  (evmap, decls, revt)
 
 (* tactics   *)
 
 let left_instance_tac (inst,id) continue seq=
   let open EConstr in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   match inst with
       Phantom dom->
-	if lookup (id,None) seq then
+	if lookup sigma (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
+	  tclTHENS (cut dom)
 	    [tclTHENLIST
-	       [Proofview.V82.of_tactic introf;
-                pf_constr_of_global id (fun idc ->
-		(fun gls-> Proofview.V82.of_tactic (generalize
-		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
-		Proofview.V82.of_tactic introf;
+	       [introf;
+                (pf_constr_of_global id >>= fun idc ->
+                Proofview.Goal.enter { enter = begin fun gl ->
+                  let id0 = List.nth (pf_ids_of_hyps gl) 0 in
+                  generalize [mkApp(idc, [|mkVar id0|])]
+                end });
+		introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
-	    tclTRY (Proofview.V82.of_tactic assumption)]
-    | Real((m,t) as c,_)->
-	if lookup (id,Some c) seq then
+	    tclTRY assumption]
+    | Real((m,t),_)->
+        let c = (m, EConstr.to_constr sigma t) in
+	if lookup sigma (id,Some c) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
 	  let special_generalize=
 	    if m>0 then
-	      pf_constr_of_global id (fun idc ->
-		fun gl->
-		  let evmap,rc,ot = mk_open_instance id idc gl m t in
-		  let ot = EConstr.of_constr ot in
+	      (pf_constr_of_global id >>= fun idc ->
+		Proofview.Goal.s_enter { s_enter = begin fun gl->
+		  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
@@ -160,34 +164,38 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
-		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
+		    Sigma.Unsafe.of_pair (generalize [gt], evmap)
+                end })
 	    else
-              let t = EConstr.of_constr t in
-	      pf_constr_of_global id (fun idc ->
-		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
+	      pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
 	  in
 	    tclTHENLIST
 	      [special_generalize;
-	       Proofview.V82.of_tactic introf;
+	       introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
+  end }
 
 let right_instance_tac inst continue seq=
+  let open EConstr in
+  Proofview.Goal.enter { enter = begin fun gl ->
   match inst with
       Phantom dom ->
-	tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
+	tclTHENS (cut dom)
 	[tclTHENLIST
-	   [Proofview.V82.of_tactic introf;
-	    (fun gls->
-	       Proofview.V82.of_tactic (split (ImplicitBindings
-			[EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
+	   [introf;
+            Proofview.Goal.enter { enter = begin fun gl ->
+              let id0 = List.nth (pf_ids_of_hyps gl) 0 in
+              split (ImplicitBindings [mkVar id0])
+            end };
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY (Proofview.V82.of_tactic assumption)]
+	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t])))
+	(tclTHEN (split (ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
+  end }
 
 let instance_tac inst=
   if (snd inst)==dummy_id then
@@ -195,10 +203,10 @@ let instance_tac inst=
   else
     left_instance_tac inst
 
-let quantified_tac lf backtrack continue seq gl=
-  let insts=give_instances lf seq in
+let quantified_tac lf backtrack continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let insts=give_instances (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
-      backtrack gl
-
-
+      backtrack
+  end }
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index ce711f3f97..47550f314e 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -9,9 +9,9 @@
 open Globnames
 open Rules
 
-val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
+val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
 
-val give_instances : Formula.t list -> Sequent.t ->
+val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
   (Unify.instance * global_reference) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a60fd4d8f1..e0d2c38a73 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -10,10 +10,12 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Vars
-open Tacmach
+open Tacmach.New
 open Tactics
-open Tacticals
+open Tacticals.New
+open Proofview.Notations
 open Termops
 open Formula
 open Sequent
@@ -22,148 +24,165 @@ open Locus
 
 module NamedDecl = Context.Named.Declaration
 
+type tactic = unit Proofview.tactic
+
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
 type lseqtac= global_reference -> seqtac
 
 type 'a with_backtracking = tactic -> 'a
 
-let wrap n b continue seq gls=
+let wrap n b continue seq =
+  Proofview.Goal.nf_enter { enter = begin fun gls ->
   Control.check_for_interrupt ();
-  let nc=pf_hyps gls in
+  let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
+  let sigma = project gls in
   let rec aux i nc ctx=
     if i<=0 then seq else
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env (project gls) id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
+	    if occur_var env sigma id (pf_concl gls) ||
+	      List.exists (occur_var_in_decl env sigma id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in
+	      add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
   let seq1=aux n nc [] in
   let seq2=if b then
-    add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
-    continue seq2 gls
+    add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
+    continue seq2
+  end }
 
 let basename_of_global=function
     VarRef id->id
   | _->assert false
 
 let clear_global=function
-    VarRef id-> Proofview.V82.of_tactic (clear [id])
+    VarRef id-> clear [id]
   | _->tclIDTAC
 
 (* connection rules *)
 
-let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
-  with Not_found->tclFAIL 0 (Pp.str "No axiom link")
+let axiom_tac t seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  try
+    pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
+    exact_no_check c
+  with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
+  end }
 
-let ll_atom_tac a backtrack id continue seq=
+let ll_atom_tac a backtrack id continue seq =
   let open EConstr in
   tclIFTHENELSE
-    (try
-      tclTHENLIST
-	[pf_constr_of_global (find_left a seq) (fun left ->
-	  pf_constr_of_global id (fun id -> 
-	    Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))])));
+      (tclTHENLIST
+	[(Proofview.tclEVARMAP >>= fun sigma ->
+          let gr =
+            try Proofview.tclUNIT (find_left sigma a seq)
+            with Not_found -> tclFAIL 0 (Pp.str "No link")
+          in
+          gr >>= fun gr ->
+          pf_constr_of_global gr >>= fun left ->
+	  pf_constr_of_global id >>= fun id -> 
+	    generalize [(mkApp(id, [|left|]))]);
 	 clear_global id;
-	 Proofview.V82.of_tactic intro]
-    with Not_found->tclFAIL 0 (Pp.str "No link"))
+	 intro])
     (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
 
 let and_tac backtrack continue seq=
-  tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack
+  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
 
 let or_tac backtrack continue seq=
   tclORELSE
-    (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq))))))
+    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
 let arrow_tac backtrack continue seq=
-  tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq)
+  tclIFTHENELSE intro (wrap 1 true continue seq)
     (tclORELSE
-       (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq)))
+       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
        backtrack)
 (* left connectives rules *)
 
-let left_and_tac ind backtrack id continue seq gls=
- let n=(construct_nhyps ind gls).(0) in
+let left_and_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let n=(construct_nhyps (pf_env gl) ind).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
+      [(pf_constr_of_global id >>= simplest_elim);
        clear_global id;
-       tclDO n (Proofview.V82.of_tactic intro)])
+       tclDO n intro])
      (wrap n false continue seq)
-     backtrack gls
+     backtrack
+  end }
 
-let left_or_tac ind backtrack id continue seq gls=
-  let v=construct_nhyps ind gls in
+let left_or_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let v=construct_nhyps (pf_env gl) ind in
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n (Proofview.V82.of_tactic intro);
+       tclDO n intro;
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (pf_constr_of_global id >>= simplest_elim)
       (Array.map f v)
-      backtrack gls
+      backtrack
+  end }
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
+  Tacticals.New.pf_constr_of_global id >>= simplest_elim
 
 (* left arrow connective rules *)
 
 (* We use this function for false, and, or, exists *)
 
-let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
-     let rcs=ind_hyps 0 indu largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+     let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in
      let vargs=Array.of_list largs in
              (* construire le terme  H->B, le generaliser etc *)
      let myterm idc i=
        let rc=rcs.(i) in
        let p=List.length rc in
+       let u = EInstance.make u in
        let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
        let head=mkApp ((lift p idc),[|capply|]) in
-         EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
+         EConstr.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in
+       let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
+	      [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc));
 	       clear_global id;
-	       tclDO lp (Proofview.V82.of_tactic intro)])
-	   (wrap lp false continue seq) backtrack gl
+	       tclDO lp intro])
+	   (wrap lp false continue seq) backtrack
+  end }
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
   let open Vars in
-  let a = EConstr.of_constr a in
-  let b = EConstr.of_constr b in
-  let c = EConstr.of_constr c in
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d idc = mkLambda (Anonymous,b,
 		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (Proofview.V82.of_tactic (cut c))
+      (tclTHENS (cut c)
 	 [tclTHENLIST
-	    [Proofview.V82.of_tactic introf;
+	    [introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
+	  tclTHENS (cut cc)
+            [(pf_constr_of_global id >>= fun c -> exact_no_check c);
 	     tclTHENLIST
-	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
+	       [(pf_constr_of_global id >>= fun idc -> generalize [d idc]);
 		clear_global id;
-		Proofview.V82.of_tactic introf;
-		Proofview.V82.of_tactic introf;
+		introf;
+		introf;
 		tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
@@ -171,38 +190,40 @@ let ll_arrow_tac a b c backtrack id continue seq=
 
 let forall_tac backtrack continue seq=
   tclORELSE
-    (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq)
+    (tclIFTHENELSE intro (wrap 0 true continue seq)
        (tclORELSE
-	  (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq)))
+	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
        backtrack)
 
-let left_exists_tac ind backtrack id continue seq gls=
-  let n=(construct_nhyps ind gls).(0) in
+let left_exists_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let n=(construct_nhyps (pf_env gl) ind).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
       (tclTHENLIST [clear_global id;
-                    tclDO n (Proofview.V82.of_tactic intro);
+                    tclDO n intro;
                     (wrap (n-1) false continue seq)])
       backtrack
-      gls
+  end }
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
-    (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod)))
+    (tclTHENS (cut prod)
        [tclTHENLIST
-	  [Proofview.V82.of_tactic intro;
-           pf_constr_of_global id (fun idc ->
-	   (fun gls->
+	  [intro;
+           (pf_constr_of_global id >>= fun idc ->
+	   Proofview.Goal.enter { enter = begin fun gls->
               let open EConstr in
-	      let id0=pf_nth_hyp_id gls 1 in
+	      let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
+              tclTHEN (generalize [term]) (clear [id0])
+           end });
 	   clear_global id;
-	   Proofview.V82.of_tactic intro;
+	   intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
 	tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
@@ -214,12 +235,13 @@ let ll_forall_tac prod backtrack id continue seq=
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
 
 let normalize_evaluables=
-  onAllHypsAndConcl
-    (function
-	 None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
-       | Some id ->
-	   Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
+  Proofview.Goal.enter { enter = begin fun gl ->
+    unfold_in_concl (Lazy.force defined_connectives) <*>
+    tclMAP
+      (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+      (pf_ids_of_hyps gl)
+  end }
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 381b7cd87c..80a7ae2c25 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -7,10 +7,13 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Tacmach
 open Names
 open Globnames
 
+type tactic = unit Proofview.tactic
+
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
 type lseqtac= global_reference -> seqtac
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index fb0c22c2b7..59b842c825 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open CErrors
 open Util
 open Formula
@@ -57,11 +58,11 @@ end
 
 module OrderedConstr=
 struct
-  type t=constr
+  type t=Constr.t
   let compare=constr_ord
 end
 
-type h_item = global_reference * (int*constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -81,13 +82,15 @@ module CM=Map.Make(OrderedConstr)
 
 module History=Set.Make(Hitem)
 
-let cm_add typ nam cm=
+let cm_add sigma typ nam cm=
+  let typ = EConstr.to_constr sigma typ in
   try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
 
-let cm_remove typ nam cm=
+let cm_remove sigma typ nam cm=
+  let typ = EConstr.to_constr sigma typ in
   try
     let l=CM.find typ cm in
     let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -112,19 +115,19 @@ let deepen seq={seq with depth=seq.depth-1}
 
 let record item seq={seq with history=History.add item seq.history}
 
-let lookup item seq=
+let lookup sigma item seq=
   History.mem item seq.history ||
   match item with
       (_,None)->false
-    | (id,Some ((m,t) as c))->
+    | (id,Some (m, t))->
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in
+	    | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
 	  History.exists p seq.history
 
-let add_formula side nam t seq gl=
-  match build_formula side nam t gl seq.cnt with
+let add_formula env sigma side nam t seq =
+  match build_formula env sigma side nam t seq.cnt with
       Left f->
 	begin
 	  match side with
@@ -136,7 +139,7 @@ let add_formula side nam t seq gl=
 	    | _ ->
 		{seq with
 		   redexes=HP.add f seq.redexes;
-		   context=cm_add f.constr nam seq.context}
+		   context=cm_add sigma f.constr nam seq.context}
 	end
     | Right t->
 	match side with
@@ -144,18 +147,18 @@ let add_formula side nam t seq gl=
 	      {seq with gl=t;glatom=Some t}
 	  | _ ->
 	      {seq with
-		 context=cm_add t nam seq.context;
+		 context=cm_add sigma t nam seq.context;
 		 latoms=t::seq.latoms}
 
-let re_add_formula_list lf seq=
+let re_add_formula_list sigma lf seq=
   let do_one f cm=
     if f.id == dummy_id then cm
-    else cm_add f.constr f.id cm in
+    else cm_add sigma f.constr f.id cm in
   {seq with
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
-let find_left t seq=List.hd (CM.find t seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
 
 (*let rev_left seq=
   try
@@ -164,7 +167,7 @@ let find_left t seq=List.hd (CM.find t seq.context)
   with Heap.EmptyHeap -> false
 *)
 
-let rec take_formula seq=
+let rec take_formula sigma seq=
   let hd=HP.maximum seq.redexes
   and hp=HP.remove seq.redexes in
     if hd.id == dummy_id then
@@ -172,11 +175,11 @@ let rec take_formula seq=
 	if seq.gl==hd.constr then
 	  hd,nseq
 	else
-	  take_formula nseq (* discarding deprecated goal *)
+	  take_formula sigma nseq (* discarding deprecated goal *)
     else
       hd,{seq with
 	    redexes=hp;
-	    context=cm_remove hd.constr hd.id seq.context}
+	    context=cm_remove sigma hd.constr hd.id seq.context}
 
 let empty_seq depth=
   {redexes=HP.empty;
@@ -196,18 +199,17 @@ let expand_constructor_hints =
     | gr ->
 	[gr])
 
-let extend_with_ref_list l seq gl =
+let extend_with_ref_list env sigma l seq =
   let l = expand_constructor_hints l in
-  let f gr (seq,gl) =
-    let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
-    let typ = EConstr.Unsafe.to_constr typ in
-      (add_formula Hyp gr typ seq gl,gl) in
-    List.fold_right f l (seq,gl)
+  let f gr (seq, sigma) =
+    let sigma, c = Evd.fresh_global env sigma gr in
+    let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in
+      (add_formula env sigma Hyp gr typ seq, sigma) in
+    List.fold_right f l (seq, sigma)
 
 open Hints
 
-let extend_with_auto_hints l seq gl=
+let extend_with_auto_hints env sigma l seq =
   let seqref=ref seq in
   let f p_a_t =
     match repr_hint p_a_t.code with
@@ -215,10 +217,9 @@ let extend_with_auto_hints l seq gl=
       | Res_pf_THEN_trivial_fail (c,_) ->
           let (c, _, _) = c in
 	  (try
-	     let (gr, _) = Termops.global_of_constr (project gl) c in
-	     let typ=(pf_unsafe_type_of gl c) in
-	     let typ = EConstr.Unsafe.to_constr typ in
-	       seqref:=add_formula Hint gr typ !seqref gl
+	     let (gr, _) = Termops.global_of_constr sigma c in
+	     let typ=(Typing.unsafe_type_of env sigma c) in
+	       seqref:=add_formula env sigma Hint gr typ !seqref
 	   with Not_found->())
       | _-> () in
   let g _ _ l = List.iter f l in
@@ -230,7 +231,7 @@ let extend_with_auto_hints l seq gl=
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
     List.iter h l;
-    !seqref, gl (*FIXME: forgetting about universes*)
+    !seqref, sigma (*FIXME: forgetting about universes*)
 
 let print_cmap map=
   let print_entry c l s=
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 06c9251e7b..18d68f54f9 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -7,22 +7,23 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Formula
 open Tacmach
 open Globnames
 
-module OrderedConstr: Set.OrderedType with type t=constr
+module OrderedConstr: Set.OrderedType with type t=Constr.t
 
-module CM: CSig.MapS with type key=constr
+module CM: CSig.MapS with type key=Constr.t
 
-type h_item = global_reference * (int*constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module History: Set.S with type elt = h_item
 
-val cm_add : constr -> global_reference -> global_reference list CM.t ->
+val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
 
-val cm_remove : constr -> global_reference -> global_reference list CM.t ->
+val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
 
 module HP: Heap.S with type elt=Formula.t
@@ -40,23 +41,22 @@ val deepen: t -> t
 
 val record: h_item -> t -> t
 
-val lookup: h_item -> t -> bool
+val lookup: Evd.evar_map -> h_item -> t -> bool
 
-val add_formula : side -> global_reference -> constr -> t ->
-  Proof_type.goal sigma -> t
+val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t
 
-val re_add_formula_list : Formula.t list -> t -> t
+val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t
 
-val find_left : constr -> t -> global_reference
+val find_left : Evd.evar_map -> constr -> t -> global_reference
 
-val take_formula : t -> Formula.t * t
+val take_formula : Evd.evar_map -> t -> Formula.t * t
 
 val empty_seq : int -> t
 
-val extend_with_ref_list : global_reference list ->
-  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
+val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list ->
+  t -> t * Evd.evar_map
 
-val extend_with_auto_hints : Hints.hint_db_name list ->
-  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
+val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list ->
+  t -> t * Evd.evar_map
 
 val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 7cbfb8e7de..49bf07155f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Term
+open EConstr
 open Vars
 open Termops
 open Reductionops
@@ -21,13 +22,12 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
-let strip_outer_cast t =
-  EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
-
 let pop t = Vars.lift (-1) t
+let subst_meta subst t =
+  let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in
+  EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t))
 
-let unif t1 t2=
-  let evd = Evd.empty in (** FIXME *)
+let unif evd t1 t2=
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -35,7 +35,7 @@ let unif t1 t2=
       (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
   let rec head_reduce t=
     (* forbids non-sigma-normal meta in head position*)
-    match kind_of_term t with
+    match EConstr.kind evd t with
 	Meta i->
 	  (try
 	     head_reduce (Int.List.assoc i !sigma)
@@ -44,25 +44,25 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
-      and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
-	match (kind_of_term nt1),(kind_of_term nt2) with
+      let nt1=head_reduce (whd_betaiotazeta evd t1)
+      and nt2=head_reduce (whd_betaiotazeta evd t2) in
+	match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
 		if i<j then bind j nt1
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
-		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
+		if Int.Set.is_empty (free_rels evd t) &&
+		  not (occur_term evd (EConstr.mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
-		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
+		if Int.Set.is_empty (free_rels evd t) &&
+		  not (occur_term evd (EConstr.mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
+	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
 	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
@@ -84,19 +84,19 @@ let unif t1 t2=
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
 		  done
-	  | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2))
+	  | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
       assert false
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
-let value i t=
+let value evd i t=
   let add x y=
     if x<0 then y else if y<0 then x else x+y in
   let rec vaux term=
-    if isMeta term && Int.equal (destMeta term) i then 0 else
+    if isMeta evd term && Int.equal (destMeta evd term) i then 0 else
       let f v t=add v (vaux t) in
-      let vr=fold_constr f (-1) term in
+      let vr=EConstr.fold evd f (-1) term in
 	if vr<0 then -1 else vr+1 in
     vaux t
 
@@ -104,11 +104,11 @@ type instance=
     Real of (int*constr)*int
   | Phantom of constr
 
-let mk_rel_inst t=
+let mk_rel_inst evd t=
   let new_rel=ref 1 in
   let rel_env=ref [] in
   let rec renum_rec d t=
-    match kind_of_term t with
+    match EConstr.kind evd t with
 	Meta n->
 	  (try
 	     mkRel (d+(Int.List.assoc n !rel_env))
@@ -117,15 +117,15 @@ let mk_rel_inst t=
 	       incr new_rel;
 	       rel_env:=(n,m) :: !rel_env;
 	       mkRel (m+d))
-      | _ -> map_constr_with_binders succ renum_rec d t
+      | _ -> EConstr.map_with_binders evd succ renum_rec d t
   in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
 
-let unif_atoms i dom t1 t2=
+let unif_atoms evd i dom t1 t2=
   try
-    let t=Int.List.assoc i (unif t1 t2) in
-      if isMeta t then Some (Phantom dom)
-      else Some (Real(mk_rel_inst t,value i t1))
+    let t=Int.List.assoc i (unif evd t1 t2) in
+      if isMeta evd t then Some (Phantom dom)
+      else Some (Real(mk_rel_inst evd t,value evd i t1))
   with
       UFAIL(_,_) ->None
     | Not_found ->Some (Phantom dom)
@@ -134,11 +134,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
   let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
-let more_general (m1,t1) (m2,t2)=
+let more_general evd (m1,t1) (m2,t2)=
   let mt1=renum_metas_from 0 m1 t1
   and mt2=renum_metas_from m1 m2 t2 in
     try
-      let sigma=unif mt1 mt2 in
-      let p (n,t)= n<m1 || isMeta t in
+      let sigma=unif evd mt1 mt2 in
+      let p (n,t)= n<m1 || isMeta evd t in
 	List.for_all p sigma
     with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 4fe9ad38d8..c9cca9bd8d 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -7,15 +7,16 @@
 (************************************************************************)
 
 open Term
+open EConstr
 
 exception UFAIL of constr*constr
 
-val unif : constr -> constr -> (int*constr) list
+val unif : Evd.evar_map -> constr -> constr -> (int*constr) list
 
 type instance=
     Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr        (* domaine de quantification *)
 
-val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
+val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
 
-val more_general : (int*constr) -> (int*constr) -> bool
+val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index e11cbc279a..25d8f8c832 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -617,9 +617,9 @@ let rec fourier () =
       			        [Tacticals.New.tclORELSE
                                    (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
                                    (Proofview.tclUNIT ());
-				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
+				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq ->
 					  (Tacticals.New.tclTHEN (apply symeq)
-						(apply (get coq_Rinv_1))))]
+						(apply (get coq_Rinv_1)))]
 
 					 )
 				]));
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c7943..ff5e7d5ff2 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -85,7 +85,7 @@ TACTIC EXTEND not_evar
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+  [ "is_ground" constr(ty) ] -> [ is_ground ty ]
 END
 
 TACTIC EXTEND autoapply
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf55..fdcaedab3a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -19,6 +19,7 @@ open Geninterp
 open Extraargs
 open Tacmach
 open Tacticals
+open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
+  Proofview.Goal.enter { enter = begin fun gl ->
   let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    Tacticals.New.tclMAP
       (fun cl ->
         match cl with
-          | Some id when is_tac id -> tclIDTAC
-          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+          | Some id when is_tac id -> Tacticals.New.tclIDTAC
+          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+      (None :: List.map (fun id -> Some id) hyps)
+  end }
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
 
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..12a1566e20 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2197,7 +2197,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
-  Proofview.V82.tactic (fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2212,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-   Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-      gl)
+  end }
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 4b87e6e2ed..eb26c5431d 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -901,16 +901,13 @@ struct
    coq_Qeq, Mc.OpEq
   ]
 
-  let has_typ gl t1 typ = 
-   let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
-   EConstr.eq_constr (Tacmach.project gl) ty typ
-
+  type gl = { env : Environ.env; sigma : Evd.evar_map }
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
+   Reductionops.is_conv gl.env gl.sigma t1 t2
 
   let parse_zop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
     | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
     | Ind((n,0),_) ->
@@ -920,7 +917,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_rop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
      | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
      | Ind((n,0),_) ->
@@ -930,7 +927,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_qop gl (op,args) =
-    (assoc_const (Tacmach.project gl) op qop_table, args.(0) , args.(1))
+    (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
 
   let is_constant sigma t = (* This is an approx *)
    match EConstr.kind sigma t with
@@ -1154,7 +1151,7 @@ struct
    rop_spec
 
   let  parse_arith parse_op parse_expr env cstr gl =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
    if debug
    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
    match EConstr.kind sigma cstr with
@@ -1199,7 +1196,7 @@ struct
     *)
   
   let parse_formula gl parse_atom env tg term =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
 
     let parse_atom env tg t =
       try
@@ -1208,7 +1205,7 @@ struct
       with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) term in 
+      let sort  = Retyping.get_sort_of gl.env gl.sigma term in 
      Sorts.is_prop sort in
      
     let rec xparse_formula env tg term =
@@ -1720,7 +1717,6 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-   let gl = Tacmach.New.of_old (fun x -> x) gl in
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1730,7 +1726,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
        ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.pf_concl gl))
+      (Tacmach.New.pf_concl gl))
   ] 
   end }
 
@@ -1967,11 +1963,13 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
     Some (ids,ff',res')
 
 
-
 (**
   * Parse the proof environment, and call micromega_tauto
   *)
 
+let fresh_id avoid id gl =
+  Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 let micromega_gen
     parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -1979,17 +1977,17 @@ let micromega_gen
     unsat deduce 
     spec dumpexpr prover tac =
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
-    let sigma = Tacmach.project gl in
-    let concl = Tacmach.pf_concl gl in
-    let hyps  = Tacmach.pf_hyps_types gl in
+    let sigma = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let hyps  = Tacmach.New.pf_hyps_types gl in
     try
-     let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+     let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+     let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
      let env = Env.elements env in
      let spec = Lazy.force spec in
      let dumpexpr = Lazy.force dumpexpr in
      
-     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl with
+     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl0 with
      | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
      | Some (ids,ff',res') -> 
        let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in
@@ -1998,7 +1996,7 @@ let micromega_gen
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
 
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
@@ -2057,7 +2055,6 @@ let micromega_order_changer cert env ff  =
   let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
   let vm = dump_varmap (typ) (vm_of_list env) in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -2069,7 +2066,7 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.pf_concl gl)));
+        (Tacmach.New.pf_concl gl)));
      (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
   end }
@@ -2088,20 +2085,20 @@ let micromega_genr prover tac =
     dump_proof = dump_psatz coq_Q dump_q
   } in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-     let gl = Tacmach.New.of_old (fun x -> x) gl in
-     let sigma = Tacmach.project gl in
-     let concl = Tacmach.pf_concl gl in
-     let hyps  = Tacmach.pf_hyps_types gl in
+     let sigma = Tacmach.New.project gl in
+     let concl = Tacmach.New.pf_concl gl in
+     let hyps  = Tacmach.New.pf_hyps_types gl in
 
      try
-      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+      let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+      let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
        let env = Env.elements env in
        let spec = Lazy.force spec in
        
        let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
        let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
        
-       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
+       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl0 with
        | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") 
        | Some (ids,ff',res') -> 
          let (ff,ids) = formula_hyps_concl 
@@ -2114,7 +2111,7 @@ let micromega_genr prover tac =
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
        
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 7780de7127..92b092ffe9 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -19,8 +19,8 @@ open Names
 open Nameops
 open Term
 open EConstr
-open Tacticals
-open Tacmach
+open Tacticals.New
+open Tacmach.New
 open Tactics
 open Logic
 open Libnames
@@ -41,7 +41,9 @@ let elim_id id =
   Proofview.Goal.enter { enter = begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end }
-let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
+let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
+  apply (Tacmach.New.pf_global id gl)
+end }
 
 let timing timer_name f arg = f arg
 
@@ -146,14 +148,14 @@ let intern_id,unintern_id,reset_intern_tables =
        Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
   (fun () -> cpt := 0; Hashtbl.clear table)
 
-let mk_then = tclTHENLIST
+let mk_then tacs = tclTHENLIST tacs
 
 let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
 let generalize_tac t = generalize t
 let elim t = simplest_elim t
-let exact t = Tacmach.refine t
 let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
+let pf_nf gl c = pf_apply Tacred.simpl gl c
 
 let rev_assoc k =
   let rec loop = function
@@ -580,9 +582,12 @@ let abstract_path sigma typ path t =
   let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
-let focused_simpl path gl =
+let focused_simpl path =
+  let open Tacmach.New in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
+  convert_concl_no_check newc DEFAULTcast
+  end }
 
 let focused_simpl path = focused_simpl path
 
@@ -640,11 +645,19 @@ let decompile af =
   in
   loop af.body
 
-let mkNewMeta () = mkMeta (Evarutil.new_meta())
+(** Backward compat to emulate the old Refine: normalize the goal conclusion *)
+let new_hole env sigma c =
+  let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in
+  Evarutil.new_evar env sigma c
 
-let clever_rewrite_base_poly typ p result theorem gl =
+let clever_rewrite_base_poly typ p result theorem =
+  let open Tacmach.New in
+  let open Sigma in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let full = pf_concl gl in
+  let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
+  Refine.refine { run = begin fun sigma ->
   let t =
     applist
       (mkLambda
@@ -657,13 +670,17 @@ let clever_rewrite_base_poly typ p result theorem gl =
 		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted])
   in
-  exact (applist(t,[mkNewMeta()])) gl
+  let argt = mkApp (abstracted, [|result|]) in
+  let Sigma (hole, sigma, p) = new_hole env sigma argt in
+  Sigma (applist (t, [hole]), sigma, p)
+  end }
+  end }
 
-let clever_rewrite_base p result theorem gl =
-  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+let clever_rewrite_base p result theorem =
+  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
 
-let clever_rewrite_base_nat p result theorem gl =
-  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+let clever_rewrite_base_nat p result theorem =
+  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem
 
 let clever_rewrite_gen p result (t,args) =
   let theorem = applist(t, args) in
@@ -673,12 +690,29 @@ let clever_rewrite_gen_nat p result (t,args) =
   let theorem = applist(t, args) in
   clever_rewrite_base_nat p result theorem
 
-let clever_rewrite p vpath t gl =
+(** Solve using the term the term [t _] *)
+let refine_app gl t =
+  let open Tacmach.New in
+  let open Sigma in
+  Refine.refine { run = begin fun sigma ->
+  let env = pf_env gl in
+  let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with
+  | Prod (_, t, _) -> t
+  | _ -> assert false
+  in
+  let Sigma (hole, sigma, p) = new_hole env sigma ht in
+  Sigma (applist (t, [hole]), sigma, p)
+  end }
+
+let clever_rewrite p vpath t =
+  let open Tacmach.New in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
-  exact (applist(t',[mkNewMeta()])) gl
+  refine_app gl t'
+  end }
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -942,15 +976,15 @@ let rec transform sigma p t =
 	  transform sigma p
 	    (mkApp (Lazy.force coq_Zplus,
 		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
-	Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
+	unfold sp_Zminus :: tac,t
     | Kapp(Zsucc,[t1]) ->
 	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer one |])) in
-	Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
+	unfold sp_Zsucc :: tac,t
     | Kapp(Zpred,[t1]) ->
 	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer negone |])) in
-	Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
+	unfold sp_Zpred :: tac,t
    | Kapp(Zmult,[t1;t2]) ->
        let tac1,t1' = transform sigma (P_APP 1 :: p) t1
        and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
@@ -1068,7 +1102,7 @@ let replay_history tactic_normalisation =
       | HYP e :: l ->
 	  begin
 	    try
-	      Tacticals.New.tclTHEN
+	      tclTHEN
 		(Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
 		(loop l)
 	    with Not_found -> loop l end
@@ -1080,16 +1114,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
-	  Tacticals.New.tclTHENLIST [
+	  tclTHENLIST [
 	    generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
 		mkVar id1; mkVar id2 |])];
-	    Proofview.V82.tactic (mk_then tac);
+	    mk_then tac;
 	    (intros_using [aux]);
-	    Proofview.V82.tactic (resolve_id aux);
+	    resolve_id aux;
             reflexivity
           ]
       | CONTRADICTION (e1,e2) :: l ->
@@ -1104,8 +1138,8 @@ let replay_history tactic_normalisation =
 					Lazy.force coq_Gt;
 					Lazy.force coq_Gt |])
 	    in
-            Tacticals.New.tclTHENS
-	      (Tacticals.New.tclTHENLIST [
+            tclTHENS
+	      (tclTHENLIST [
 		unfold sp_Zle;
 		simpl_in_concl;
 		intro;
@@ -1118,7 +1152,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
+	  Proofview.tclTHEN (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)
@@ -1128,10 +1162,10 @@ 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
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut state_eg)
-	    [ Tacticals.New.tclTHENS
-	        (Tacticals.New.tclTHENLIST [
+	    [ tclTHENS
+	        (tclTHENLIST [
 		  (intros_using [aux]);
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
@@ -1139,9 +1173,9 @@ let replay_history tactic_normalisation =
 		  (clear [aux;id]);
 		  (intros_using [id]);
 		  (cut (mk_gt kk dd)) ])
-	        [ Tacticals.New.tclTHENS
+	        [ tclTHENS
 		    (cut (mk_gt kk izero))
-		    [ Tacticals.New.tclTHENLIST [
+		    [ tclTHENLIST [
 		        (intros_using [aux1; aux2]);
 		        (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
@@ -1149,13 +1183,13 @@ let replay_history tactic_normalisation =
 		        (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
-		      Tacticals.New.tclTHENLIST [
+		      tclTHENLIST [
 			(unfold sp_Zgt);
 			simpl_in_concl;
 			reflexivity ] ];
-		  Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
+		  tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
                 ];
-	      Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+	      tclTHEN (mk_then tac) reflexivity ]
 
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
 	  let c = floor_div e1.constant k in
@@ -1166,10 +1200,10 @@ 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
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut (mk_gt dd izero))
-	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
-		[Tacticals.New.tclTHENLIST [
+	    [ tclTHENS (cut (mk_gt kk dd))
+		[tclTHENLIST [
 		  (intros_using [aux2;aux1]);
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
@@ -1177,14 +1211,14 @@ let replay_history tactic_normalisation =
 		  (clear [aux1;aux2]);
 		  unfold sp_not;
 		  (intros_using [aux]);
-		  Proofview.V82.tactic (resolve_id aux);
-		  Proofview.V82.tactic (mk_then tac);
+		  resolve_id aux;
+		  mk_then tac;
 		  assumption ] ;
-		 Tacticals.New.tclTHENLIST [
+		 tclTHENLIST [
 		   unfold sp_Zgt;
 		   simpl_in_concl;
 		   reflexivity ] ];
-              Tacticals.New.tclTHENLIST [
+              tclTHENLIST [
 		unfold sp_Zgt;
                 simpl_in_concl;
 		reflexivity ] ]
@@ -1197,9 +1231,9 @@ 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
-            Tacticals.New.tclTHENS
+            tclTHENS
 	      (cut state_eq)
-	      [Tacticals.New.tclTHENLIST [
+	      [tclTHENLIST [
 		(intros_using [aux1]);
 		(generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
@@ -1207,14 +1241,14 @@ let replay_history tactic_normalisation =
 		(clear [aux1;id]);
 		(intros_using [id]);
 		(loop l) ];
-	       Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+	       tclTHEN (mk_then tac) reflexivity ]
 	  else
             let tac = scalar_norm [P_APP 3] e2.body in
-            Tacticals.New.tclTHENS (cut state_eq)
+            tclTHENS (cut state_eq)
 	      [
-		Tacticals.New.tclTHENS
+		tclTHENS
 		 (cut (mk_gt kk izero))
-		 [Tacticals.New.tclTHENLIST [
+		 [tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
@@ -1222,11 +1256,11 @@ let replay_history tactic_normalisation =
 		   (clear [aux1;aux2;id]);
 		   (intros_using [id]);
 		   (loop l) ];
-		  Tacticals.New.tclTHENLIST [
+		  tclTHENLIST [
 		    unfold sp_Zgt;
                     simpl_in_concl;
 		    reflexivity ] ];
-		Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+		tclTHEN (mk_then tac) reflexivity ]
       | (MERGE_EQ(e3,e1,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1239,16 +1273,16 @@ let replay_history tactic_normalisation =
 	      (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
             scalar_norm [P_APP 3] e1.body
 	  in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut (mk_eq eq1 (mk_inv eq2)))
-	    [Tacticals.New.tclTHENLIST [
+	    [tclTHENLIST [
 	      (intros_using [aux]);
 	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
 	      (clear [id1;id2;aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
+            tclTHEN (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 ()
@@ -1272,9 +1306,9 @@ 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
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut theorem)
-	    [Tacticals.New.tclTHENLIST [
+	    [tclTHENLIST [
 	      (intros_using [aux]);
 	      (elim_id aux);
 	      (clear [aux]);
@@ -1282,11 +1316,11 @@ let replay_history tactic_normalisation =
 	      (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
-	      Proofview.V82.tactic (mk_then tac);
+	      mk_then tac;
 	      (clear [aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
+            tclTHEN (exists_tac eq1) reflexivity ]
       | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
 	  let id1 = new_identifier ()
 	  and id2 = new_identifier () in
@@ -1295,10 +1329,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
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
-	    [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) ]]
+	    [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ];
+             tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]]
       | SUM(e3,(k1,e1),(k2,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1317,10 +1351,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
-            Tacticals.New.tclTHENLIST [
+            tclTHENLIST [
 	      (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
-	      Proofview.V82.tactic (mk_then tac);
+	      mk_then tac;
 	      (intros_using [id]);
 	      (loop l)
             ]
@@ -1329,10 +1363,10 @@ 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
-            Tacticals.New.tclTHENS (cut (mk_gt kk1 izero))
-	      [Tacticals.New.tclTHENS
+            tclTHENS (cut (mk_gt kk1 izero))
+	      [tclTHENS
 		 (cut (mk_gt kk2 izero))
-		 [Tacticals.New.tclTHENLIST [
+		 [tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
@@ -1340,29 +1374,29 @@ let replay_history tactic_normalisation =
 		       mkVar aux1;mkVar aux2;
 		       mkVar id1;mkVar id2 |])]);
 		   (clear [aux1;aux2]);
-		   Proofview.V82.tactic (mk_then tac);
+		   mk_then tac;
 		   (intros_using [id]);
 		   (loop l) ];
-		 Tacticals.New.tclTHENLIST [
+		 tclTHENLIST [
 		   unfold sp_Zgt;
                    simpl_in_concl;
 		   reflexivity ] ];
-	      Tacticals.New.tclTHENLIST [
+	      tclTHENLIST [
 		unfold sp_Zgt;
                 simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+	  tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
+	  tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
-	  Tacticals.New.tclTHENLIST [
+	  tclTHENLIST [
 	    (generalize_tac [mkVar (hyp_of_tag e)]);
             unfold sp_Zle;
 	    simpl_in_concl;
 	    unfold sp_not;
 	    (intros_using [aux]);
-	    Proofview.V82.tactic (resolve_id aux);
+	    resolve_id aux;
 	    reflexivity
           ]
       | _ -> Proofview.tclUNIT ()
@@ -1380,12 +1414,12 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize sigma p_initial t in
   let shift_left =
     tclTHEN
-      (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
-      (tclTRY (Proofview.V82.of_tactic (clear [id])))
+      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (tclTRY (clear [id]))
   in
   if not (List.is_empty tac) then
     let id' = new_identifier () in
-    ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ]))
+    ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ]))
           :: tactic,
      compile id' flag t' :: defs)
   else
@@ -1430,7 +1464,7 @@ let destructure_omega gl tac_def (id,c) =
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
-  Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id)
+  tclTHEN (tclTRY (clear [id])) (intro_using id)
 
 
 open Proofview.Notations
@@ -1449,7 +1483,7 @@ let coq_omega =
            let id = new_identifier () in
            let i = new_id () in
            tag_hypothesis id i;
-           (Tacticals.New.tclTHENLIST [
+           (tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
 	     (intros_using [v; id]);
 	     (elim_id id);
@@ -1460,7 +1494,7 @@ let coq_omega =
 	    body = [{v=intern_id v; c=one}];
             constant = zero; id = i} :: sys
 	 else
-           (Tacticals.New.tclTHENLIST [
+           (tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_new_var, [t])));
 	     (intros_using [v;th]);
 	     tac ]),
@@ -1476,13 +1510,13 @@ let coq_omega =
     with UNSOLVABLE ->
       let _,path = depend [] [] (history ()) in
       if !display_action_flag then display_action display_var path;
-      (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path))
+      (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;
-      Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
+      tclTHEN prelude (replay_history tactic_normalisation path)
+    with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
   end
   end }
 
@@ -1495,36 +1529,36 @@ let nat_inject =
     Proofview.tclEVARMAP >>= fun sigma ->
     try match destructurate_term sigma t with
       | Kapp(Plus,[t1;t2]) ->
-          Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+          tclTHENLIST [
+	    (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]) ->
-          Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+          tclTHENLIST [
+	    (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
-          Tacticals.New.tclTHENS
-            (Tacticals.New.tclTHEN
+          tclTHENS
+            (tclTHEN
 	       (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
 	       (intros_using [id]))
 	    [
-	      Tacticals.New.tclTHENLIST [
-	        Proofview.V82.tactic (clever_rewrite_gen p
+	      tclTHENLIST [
+	        (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) ];
-	      (Tacticals.New.tclTHEN
-		 (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero)
-                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])))
+	      (tclTHEN
+		 (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']) ->
@@ -1538,24 +1572,24 @@ let nat_inject =
           let rec loop p t : unit Proofview.tactic =
             try match destructurate_term sigma t with
 		Kapp(S,[t]) ->
-                  (Tacticals.New.tclTHEN
-                     (Proofview.V82.tactic (clever_rewrite_gen p
+                  (tclTHEN
+                     (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 Proofview.V82.tactic (focused_simpl p) else loop p t
+          if is_number t' then 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
-          Tacticals.New.tclTHEN
-            (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
-               ((Lazy.force coq_pred_of_minus),[t])))
+          tclTHEN
+            (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,[]) -> Proofview.V82.tactic (focused_simpl p)
+      | Kapp(O,[]) -> focused_simpl p
       | _ -> Proofview.tclUNIT ()
     with e when catchable_exception e -> Proofview.tclUNIT ()
 
@@ -1565,7 +1599,7 @@ let nat_inject =
         Proofview.tclEVARMAP >>= fun sigma ->
 	  begin try match destructurate_prop sigma t with
               Kapp(Le,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1574,7 +1608,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Lt,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1583,7 +1617,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Ge,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1592,7 +1626,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Gt,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1601,7 +1635,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Neq,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1611,7 +1645,7 @@ let nat_inject =
                 ]
             | Kapp(Eq,[typ;t1;t2]) ->
 		if is_conv typ (Lazy.force coq_nat) then
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
@@ -1697,20 +1731,20 @@ let fresh_id avoid id gl =
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.enter { enter = begin fun gl ->
+  tclTHEN
+    (tclTRY (clear [id]))
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id = fresh_id [] id gl in
-     Tacticals.New.tclTHEN (introduction id) (tac id)
+     tclTHEN (introduction id) (tac id)
     end })
 
 let onClearedName2 id tac =
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.enter { enter = begin fun gl ->
+  tclTHEN
+    (tclTRY (clear [id]))
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id1 = fresh_id [] (add_suffix id "_left") gl in
      let id2 = fresh_id [] (add_suffix id "_right") gl in
-      Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
+      tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end })
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
@@ -1724,7 +1758,7 @@ let destructure_hyps =
   let decidability = decidability gl in
   let pf_nf = pf_nf gl in
     let rec loop = function
-      | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
+      | [] -> (tclTHEN nat_inject coq_omega)
       | decl::lit ->
           let i = NamedDecl.get_id decl in
           Proofview.tclEVARMAP >>= fun sigma ->
@@ -1732,17 +1766,17 @@ let destructure_hyps =
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
-              (Tacticals.New.tclTHENS
+              (tclTHENS
                  (elim_id i)
                  [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit)));
                    onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
-              Tacticals.New.tclTHEN
+              tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit)))
           | Kapp(Iff,[t1;t2]) ->
-	      Tacticals.New.tclTHEN
+	      tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit)))
@@ -1752,7 +1786,7 @@ let destructure_hyps =
               if is_Prop sigma (type_of t2)
               then
 		let d1 = decidability t1 in
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
@@ -1763,7 +1797,7 @@ let destructure_hyps =
           | Kapp(Not,[t]) ->
               begin match destructurate_prop sigma t with
 		Kapp(Or,[t1;t2]) ->
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1771,7 +1805,7 @@ let destructure_hyps =
                   ]
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
@@ -1781,7 +1815,7 @@ let destructure_hyps =
 	      | Kapp(Iff,[t1;t2]) ->
 		  let d1 = decidability t1 in
 		  let d2 = decidability t2 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
@@ -1793,7 +1827,7 @@ let destructure_hyps =
 		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
 		       For t1, being decidable implies being Prop. *)
 		  let d1 = decidability t1 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
@@ -1802,7 +1836,7 @@ let destructure_hyps =
                   ]
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
@@ -1810,7 +1844,7 @@ let destructure_hyps =
 	      | Kapp(op,[t1;t2]) ->
 		  (try
 		     let thm = not_binop op in
-                     Tacticals.New.tclTHENLIST [
+                     tclTHENLIST [
 		       (generalize_tac
 			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 		       (onClearedName i (fun _ -> loop lit))
@@ -1820,14 +1854,14 @@ let destructure_hyps =
                   if !old_style_flag then begin
 		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
-                        Tacticals.New.tclTHENLIST [
+                        tclTHENLIST [
 			  (simplest_elim
 			     (mkApp
                                 (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
 			  (onClearedName i (fun _ -> loop lit))
                         ]
 		    | Kapp(Z,_) ->
-                        Tacticals.New.tclTHENLIST [
+                        tclTHENLIST [
 			  (simplest_elim
 			     (mkApp
 				(Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
@@ -1837,12 +1871,12 @@ let destructure_hyps =
                   end else begin
 		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
-                        (Tacticals.New.tclTHEN
+                        (tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
 		    | Kapp(Z,_) ->
-                        (Tacticals.New.tclTHEN
+                        (tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
@@ -1870,23 +1904,24 @@ let destructure_goal =
       Proofview.V82.wrap_exceptions prop >>= fun prop ->
       match prop with
       | Kapp(Not,[t]) ->
-          (Tacticals.New.tclTHEN
-	     (Tacticals.New.tclTHEN (unfold sp_not) intro)
+          (tclTHEN
+	     (tclTHEN (unfold sp_not) intro)
 	     destructure_hyps)
-      | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
+      | Kimp(a,b) -> (tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
       | _ ->
 	  let goal_tac =
 	    try
 	      let dec = decidability t in
-	      Tacticals.New.tclTHEN
-                (Proofview.V82.tactic (Tacmach.refine
-		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+	      tclTHEN
+                (Proofview.Goal.nf_enter { enter = begin fun gl ->
+		                         refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
+		                         end })
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 	  in
-	  Tacticals.New.tclTHEN goal_tac destructure_hyps
+	  tclTHEN goal_tac destructure_hyps
     in
     (loop concl)
   end }
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5c68078d7d..8d7ae51fc0 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -285,7 +285,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val is_scalar : Term.constr -> bool
 end
@@ -350,10 +350,12 @@ let parse_term t =
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
+let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+
 let parse_rel gl t =
   try match destructurate t with
     | Kapp("eq",[typ;t1;t2])
-      when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index af50ea0fff..ee7ff451a9 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -168,7 +168,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val is_scalar : Term.constr -> bool
   end
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 9a54ad7789..df7e5cb99e 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -38,7 +38,7 @@ let romega_tactic l =
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
        (Tactics.intros)
-       (Proofview.V82.tactic total_reflexive_omega_tactic))
+       (total_reflexive_omega_tactic))
 
 
 TACTIC EXTEND romega
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index cfe14b230c..a20589fb46 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -16,13 +17,12 @@ open OmegaSolver
 (* Especially useful debugging functions *)
 let debug = ref false
 
-let show_goal gl =
-  if !debug then (); Tacticals.tclIDTAC gl
+let show_goal = Tacticals.New.tclIDTAC
 
 let pp i = print_int i; print_newline (); flush stdout
 
 (* More readable than the prefix notation *)
-let (>>) = Tacticals.tclTHEN
+let (>>) = Tacticals.New.tclTHEN
 
 let mkApp = Term.mkApp
 
@@ -739,7 +739,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
 (* Destructuration des hypothèses et de la conclusion *)
 
 let reify_gl env gl =
-  let concl = Tacmach.pf_concl gl in
+  let concl = Tacmach.New.pf_concl gl in
   let concl = EConstr.Unsafe.to_constr concl in
   let t_concl =
     Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
@@ -760,7 +760,7 @@ let reify_gl env gl =
     | [] ->
 	if !debug then print_env_reification env;
 	[] in
-  let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
+  let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in
   (id_concl,t_concl) :: t_lhyps
 
 let rec destructurate_pos_hyp orig list_equations list_depends = function
@@ -1283,21 +1283,22 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Proofview.V82.of_tactic (Tactics.generalize
-    (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >>
-  Proofview.V82.of_tactic (Tactics.change_concl reified) >>
-  Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >>
+  Tactics.generalize
+    (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >>
+  Tactics.change_concl reified >>
+  Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
-  Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
+  Tactics.normalise_vm_in_concl >>
   (*i Alternatives to the previous line:
    - Normalisation without VM:
       Tactics.normalise_in_concl
    - Skip the conversion check and rely directly on the QED:
       Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
   i*)
-  Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I)))
+  Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
-let total_reflexive_omega_tactic gl =
+let total_reflexive_omega_tactic =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1306,9 +1307,9 @@ let total_reflexive_omega_tactic gl =
   let full_reified_goal = reify_gl env gl in
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
-  resolution env full_reified_goal systems_list gl
+  resolution env full_reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
-
+  end }
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a2fa34c05e..ee2e736120 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -59,9 +59,6 @@ module V82 : sig
      second goal *)
   val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
-  (* Principal part of the weak-progress tactical *)
-  val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-   
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
     
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0e..bc12b3ba71 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -162,31 +162,11 @@ let tclMAP tacfun l =
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
-let tclWEAK_PROGRESS tac ptree =
-  let rslt = tac ptree in
-  if Goal.V82.weak_progress rslt ptree then rslt
-  else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.")
-
-(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
-the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.progress rslt ptree then rslt
   else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
 
-(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
-   one of them being identical to the original goal *)
-let tclNOTSAMEGOAL (tac : tactic) goal =
-  let same_goal gls1 evd2 gl2 =
-    Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
-  in
-  let rslt = tac goal in
-  let {it=gls;sigma=sigma} = rslt in
-  if List.exists (same_goal goal sigma) gls
-  then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
-      (str"Tactic generated a subgoal identical to the original goal.")
-  else rslt
-
 (* Execute tac, show the names of new hypothesis names created by tac
    in the "as" format and then forget everything. From the logical
    point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 56f5facf89..e179589df2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,10 +119,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364f..42230dff17 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
-    | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+    | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
     | Unfold_nth c ->
-      Proofview.V82.tactic (fun gl ->
-       if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
-       else tclFAIL 0 (str"Unbound reference") gl)
+      Proofview.Goal.enter { enter = begin fun gl ->
+       if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+       else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+       end }
     | Extern tacast -> 
       conclPattern concl p tacast
   in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index df222eed80..54e4405d1c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,18 +221,22 @@ let auto_unif_flags freeze st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+  let open Tacmach.New in
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  let sigma = project gl in
   let (c, _, _) = c in
-  let c, gl =
+  let c, sigma =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
-        c, {gl with sigma = evd}
-    else c, gl
+        c, evd
+    else c, sigma
   in
-  let t1 = pf_unsafe_type_of gl c in
-  Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+  let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+  Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+  end }
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -455,15 +459,14 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
                    { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+             e_give_exact flags poly (c,clenv)
       | Res_pf_THEN_trivial_fail (term,cl) ->
          let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
-         let tac = Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]) in
-         Proofview.V82.tactic (tclWEAK_PROGRESS tac)
+         Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
       let tac = run_hint t tac in
@@ -1614,9 +1617,11 @@ let not_evar c =
   | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
   | _ -> Proofview.tclUNIT ()
 
-let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
-  else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+  let open Tacticals.New in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  if Evarutil.is_ground_term sigma c then tclIDTAC
+  else tclFAIL 0 (str"Not ground")
 
 let autoapply c i =
   let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972f..738cc0feba 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
 val not_evar : constr -> unit Proofview.tactic
 
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
 
 val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c82..25c28cf4ac 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,9 +97,6 @@ let _ =
 
 (* Rewriting tactics *)
 
-let tclNOTSAMEGOAL tac =
-  Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac))
-
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
 type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
 
@@ -268,6 +265,25 @@ let rewrite_elim with_evars frzevars cls c e =
   general_elim_clause with_evars flags cls c e
   end }
 
+let tclNOTSAMEGOAL tac =
+  let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let sigma = project gl in
+    let ev = goal gl in
+    tac >>= fun () ->
+    Proofview.Goal.goals >>= fun gls ->
+    let check accu gl' =
+      gl' >>= fun gl' ->
+      let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in
+      Proofview.tclUNIT accu
+    in
+    Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
+    if has_same then
+      tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
+    else
+      Proofview.tclUNIT ()
+  end }
+
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
   let open Pretype_errors in
@@ -642,8 +658,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   | Some evd ->
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
-    Tacticals.New.pf_constr_of_global sym (fun sym ->
-    Tacticals.New.pf_constr_of_global e (fun e ->
+    Tacticals.New.pf_constr_of_global sym >>= fun sym ->
+    Tacticals.New.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENLAST
       (replace_core clause l2r eq)
@@ -651,7 +667,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
          [assumption;
           tclTHEN (apply sym) assumption;
           try_prove_eq
-         ])))
+         ])
   end }
 
 let replace c1 c2 =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index daa962f1d6..83f3da30a9 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -260,22 +260,23 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* Applying a given inversion lemma  *)
 (* ================================= *)
 
-let lemInv id c gls =
+let lemInv id c =
+  Proofview.Goal.enter { enter = begin fun gls ->
   try
-    let open Tacmach in
     let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
-    Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
+    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
   with
     | NoSuchBinding ->
 	user_err 
-	  (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+	  (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
-	      pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
+	      pr_leconstr_env (pf_env gls) (project gls) c)
+  end }
 
-let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
 
 let lemInvIn id c ids =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -289,7 +290,7 @@ let lemInvIn id c ids =
       else
         (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
     in
-    ((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)))
   end }
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 90b7d6581a..c8441a8cc9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -51,10 +51,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
 let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
-let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
 let tclTHENTRY       = Refiner.tclTHENTRY
 let tclIFTHENELSE    = Refiner.tclIFTHENELSE
 let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
@@ -734,13 +732,11 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let pf_constr_of_global ref tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let (sigma, c) = Evd.fresh_global env sigma ref in
-      let c = EConstr.of_constr c in
-      Proofview.Unsafe.tclEVARS sigma <*> (tac c)
-    end }
+  let pf_constr_of_global ref =
+    Proofview.tclEVARMAP >>= fun sigma ->
+    Proofview.tclENV >>= fun env ->
+    let (sigma, c) = Evd.fresh_global env sigma ref in
+    let c = EConstr.of_constr c in
+    Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
 end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3b90ec514a..5a4ecbac75 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,10 +44,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic
 val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
@@ -265,5 +263,5 @@ module New : sig
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
 
-  val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+  val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..9c2a1d8509 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2811,20 +2811,18 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   mkProd_or_LetIn decl cl', sigma'
 
 let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.pf_env gl in
-  let ids = Tacmach.pf_ids_of_hyps gl in
-  let sigma, t = Typing.type_of env sigma c in
-  generalize_goal_gen env sigma ids i o t cl
-
-let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
-  let env = Tacmach.New.pf_env gl in
-  let ids = Tacmach.New.pf_ids_of_hyps gl in
+  let open Tacmach.New in
+  let env = pf_env gl in
+  let ids = pf_ids_of_hyps gl in
   let sigma, t = Typing.type_of env sigma c in
   generalize_goal_gen env sigma ids i o t cl
 
-let old_generalize_dep ?(with_let=false) c gl =
+let generalize_dep ?(with_let=false) c =
+  let open Tacmach.New in
+  let open Tacticals.New in
+  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = pf_env gl in
-  let sign = pf_hyps gl in
+  let sign = Proofview.Goal.hyps gl in
   let sigma = project gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
   let seek (d:named_declaration) (toquant:named_context) =
@@ -2843,11 +2841,11 @@ let old_generalize_dep ?(with_let=false) c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
+  let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
   let body =
     if with_let then
       match EConstr.kind sigma c with
-      | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value
+      | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
       | _ -> None
     else None
   in
@@ -2856,20 +2854,19 @@ let old_generalize_dep ?(with_let=false) c gl =
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
-  tclTHENLIST
-    [tclEVARS evd;
-     Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
-     Proofview.V82.of_tactic (clear (List.rev tothin'))]
-    gl
-
-let generalize_dep ?(with_let = false) c =
-  Proofview.V82.tactic (old_generalize_dep ~with_let c)
+  let tac =
+    tclTHEN
+      (apply_type cl'' (if Option.is_empty body then c::args else args))
+      (clear (List.rev tothin'))
+  in
+  Sigma.Unsafe.of_pair (tac, evd)
+  end }
 
 (**  *)
 let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let newcl, evd =
-    List.fold_right_i (new_generalize_goal gl) 0 lconstr
+    List.fold_right_i (generalize_goal gl) 0 lconstr
       (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
   let (evd, _) = Typing.type_of env evd newcl in
@@ -4724,7 +4721,7 @@ let symmetry_red allowred =
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
-        (Tacticals.New.pf_constr_of_global eq_data.sym apply)
+        (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end }
 
@@ -4820,8 +4817,8 @@ let transitivity_red allowred t =
       Tacticals.New.tclTHEN
         (convert_concl_no_check concl DEFAULTcast)
         (match t with
-	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
-	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
+	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply
+	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
    | None,eq,eq_kind ->
       match t with
       | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
diff --git a/vernac/command.ml b/vernac/command.ml
index 45ff579552..b27d8a0a35 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1198,11 +1198,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
-    let init_tac =
-      Option.map (List.map Proofview.V82.tactic) init_tac
-    in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
@@ -1235,11 +1232,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
-    let init_tac =
-      Option.map (List.map Proofview.V82.tactic) init_tac
-    in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))