Porting the firstorder plugin to the new tactic API.

13 files changed, 346 insertions, 297 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7773f6a2f..ade94e98e 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 5db8ff59a..3f438c04a 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 3c0319319..8ef6a09d0 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 d6cd7e2a0..ab1dd07c1 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 b5669463c..4fd1e38a2 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 9dc2a51a6..62f811546 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 ce711f3f9..47550f314 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 96601f74a..e0d2c38a7 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -10,10 +10,11 @@ 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
@@ -23,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
 
@@ -172,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
@@ -215,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 381b7cd87..80a7ae2c2 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 fb0c22c2b..59b842c82 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 06c9251e7..18d68f54f 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 7cbfb8e7d..49bf07155 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 4fe9ad38d..c9cca9bd8 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