Imported Upstream version 8.5~beta1+dfsg

13 files changed, 240 insertions, 244 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 79d4c5b5..62a8605a 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,13 +9,12 @@
 open Hipattern
 open Names
 open Term
+open Vars
 open Termops
-open Reductionops
 open Tacmach
 open Util
 open Declarations
-open Libnames
-open Inductiveops
+open Globnames
 
 let qflag=ref true
 
@@ -23,11 +22,11 @@ let red_flags=ref Closure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
-    if c=0 then g j1 j2 else c
+    if Int.equal c 0 then g j1 j2 else c
 
 let (==?) fg h i1 i2 j1 j2 k1 k2=
   let c=fg i1 i2 j1 j2 in
-    if c=0 then h k1 k2 else c
+    if Int.equal c 0 then h k1 k2 else c
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
@@ -44,7 +43,7 @@ let rec nb_prod_after n c=
     | _ -> 0
 
 let construct_nhyps ind gls =
-  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
   let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
   let hyp = nb_prod_after nparams in
     Array.map hyp constr_types
@@ -52,12 +51,11 @@ let construct_nhyps ind gls =
 (* 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 lp=Array.length types in
-  let myhyps i=
-    let t1=Term.prod_applist types.(i) largs in
+  let myhyps t =
+    let t1=prod_applist t largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
       fst (decompose_prod_assum t2) in
-    Array.init lp myhyps
+    Array.map myhyps types
 
 let special_nf gl=
   let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
@@ -69,14 +67,14 @@ let special_whd gl=
 
 type kind_of_formula=
     Arrow of constr*constr
-  | False of inductive*constr list
-  | And of inductive*constr list*bool
-  | Or of inductive*constr list*bool
-  | Exists of inductive*constr list
+  | False of pinductive*constr list
+  | And of pinductive*constr list*bool
+  | Or of pinductive*constr list*bool
+  | Exists of pinductive*constr list
   | Forall of constr*constr
   | Atom of constr
 
-let rec kind_of_formula gl term =
+let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
     match match_with_imp_term cciterm with
@@ -87,26 +85,26 @@ let rec kind_of_formula gl term =
 	   |_->
 	      match match_with_nodep_ind cciterm with
 		  Some (i,l,n)->
-		    let ind=destInd i in
+		    let ind,u=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
-		      if nconstr=0 then
-			False(ind,l)
+		      if Int.equal nconstr 0 then
+			False((ind,u),l)
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mib.mind_nparams in
-			    array_exists is_constant mip.mind_nf_lc in
+			    Int.equal (nb_prod 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)
 			  then
 			    Atom cciterm
 			  else
-			    if nconstr=1 then
-			      And(ind,l,is_trivial)
+			    if Int.equal nconstr 1 then
+			      And((ind,u),l,is_trivial)
 			    else
-			      Or(ind,l,is_trivial)
+			      Or((ind,u),l,is_trivial)
 		| _ ->
 		    match match_with_sigma_type cciterm with
 			Some (i,l)-> Exists((destInd i),l)
@@ -118,7 +116,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)
+let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms gl metagen side cciterm =
   let trivial =ref false
@@ -144,9 +142,9 @@ let build_atoms gl metagen side cciterm =
 	  let g i _ (_,_,t) =
 	    build_rec env polarity (lift i t) in
 	  let f l =
-	    list_fold_left_i g (1-(List.length l)) () l in
+	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
-	      array_exists (function []->true|_->false) v
+	      Array.exists (function []->true|_->false) v
 	    then trivial:=true;
 	    Array.iter f v
       | Exists(i,l)->
@@ -154,7 +152,7 @@ let build_atoms gl metagen side cciterm =
 	  let v =(ind_hyps 1 i l gl).(0) in
 	  let g i _ (_,_,t) =
 	    build_rec (var::env) polarity (lift i t) in
-	    list_fold_left_i g (2-(List.length l)) () v
+	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b
@@ -171,7 +169,7 @@ let build_atoms gl metagen side cciterm =
 	| Hyp      -> build_rec [] false cciterm
 	| Hint     ->
 	    let rels,head=decompose_prod cciterm in
-	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
+	    let env=List.rev_map (fun _->mkMeta (metagen true)) rels in
 	      build_rec env false head;trivial:=false (* special for hints *)
     end;
     (!trivial,
@@ -188,19 +186,19 @@ type right_pattern =
 
 type left_arrow_pattern=
     LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
+  | LLfalse of pinductive*constr list
+  | LLand of pinductive*constr list
+  | LLor of pinductive*constr list
   | LLforall of constr
-  | LLexists of inductive*constr list
+  | LLexists of pinductive*constr list
   | LLarrow of constr*constr*constr
 
 type left_pattern=
     Lfalse
-  | Land of inductive
-  | Lor of inductive
+  | Land of pinductive
+  | Lor of pinductive
   | Lforall of metavariable*constr*bool
-  | Lexists of inductive
+  | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
 type t={id:global_reference;
@@ -226,7 +224,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
+		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 44bbb335..29ea1e77 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,14 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Names
-open Libnames
+open Term
+open Context
+open Globnames
 
 val qflag : bool ref
 
@@ -24,9 +25,9 @@ type ('a,'b) sum = Left of 'a | Right of 'b
 
 type counter = bool -> metavariable
 
-val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
+val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
 
-val ind_hyps : int -> inductive -> constr list ->
+val ind_hyps : int -> pinductive -> constr list ->
   Proof_type.goal Tacmach.sigma -> rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
@@ -48,19 +49,19 @@ type right_pattern =
 
 type left_arrow_pattern=
     LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
+  | LLfalse of pinductive*constr list
+  | LLand of pinductive*constr list
+  | LLor of pinductive*constr list
   | LLforall of constr
-  | LLexists of inductive*constr list
+  | LLexists of pinductive*constr list
   | LLarrow of constr*constr*constr
 
 type left_pattern=
     Lfalse
-  | Land of inductive
-  | Lor of inductive
+  | Land of pinductive
+  | Lor of pinductive
   | Lforall of metavariable*constr*bool
-  | Lexists of inductive
+  | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
 type t={id: global_reference;
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 5b882036..c28da42a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -1,25 +1,23 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma"  i*)
+(*i camlp4deps: "grammar/grammar.cma"  i*)
 
 open Formula
 open Sequent
 open Ground
 open Goptions
-open Tactics
 open Tacticals
 open Tacinterp
-open Term
-open Names
-open Util
 open Libnames
 
+DECLARE PLUGIN "ground_plugin"
+
 (* declaring search depth as a global option *)
 
 let ground_depth=ref 3
@@ -57,16 +55,16 @@ let _=
 let (set_default_solver, default_solver, print_default_solver) = 
   Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
 
-VERNAC COMMAND EXTEND Firstorder_Set_Solver
+VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
-      (Vernacexpr.use_section_locality ())
-      (Tacinterp.glob_tactic t) ]
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
+      (Tacintern.glob_tactic t) ]
 END
 
-VERNAC COMMAND EXTEND Firstorder_Print_Solver
+VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> [
-    Pp.msgnl
+    Pp.msg_info
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
 END
 
@@ -82,10 +80,11 @@ let gen_ground_tac flag taco ids bases gl=
 	  | None-> snd (default_solver ()) in
       let startseq gl=
 	let seq=empty_seq !ground_depth in
-	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
-      let result=ground_tac solver startseq gl in
+        let 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
+    with reraise -> qflag:=backup;raise reraise
 
 (* special for compatibility with Intuition
 
@@ -103,12 +102,13 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
+open Pp
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference
-let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global))
-let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
+let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
+let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
+let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
 ARGUMENT EXTEND firstorder_using
   PRINTED BY pr_firstorder_using_typed
@@ -128,29 +128,31 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) l [] ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) [] l ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (Option.map eval_tactic t) [] [] ]
+     [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
 END
 
+open Proofview.Notations
 
-let default_declarative_automation gls =
-  tclORELSE
-    (tclORELSE (Auto.h_trivial [] None)
+let default_declarative_automation =
+  Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
+  Tacticals.New.tclORELSE
+    (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
     (Cctac.congruence_tac !congruence_depth []))
-    (gen_ground_tac true
-       (Some (tclTHEN
+    (Proofview.V82.tactic (gen_ground_tac true
+       (Some (Tacticals.New.tclTHEN
 		(snd (default_solver ()))
 		(Cctac.congruence_tac !congruence_depth [])))
-       [] []) gls
+       [] []))
 
 
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 7c80b9bb..2248b669 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,28 +12,27 @@ open Rules
 open Instances
 open Term
 open Tacmach
-open Tactics
 open Tacticals
-open Libnames
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
   let f coe=
     try
-      let kn=destConst (Classops.get_coercion_value coe) in
+      let kn= fst (destConst (Classops.get_coercion_value coe)) in
 	predref:=Names.Cpred.add kn !predref
-    with Invalid_argument "destConst"-> () in
+    with DestKO -> ()
+  in
     List.iter f (Classops.coercions ());
     red_flags:=
     Closure.RedFlags.red_add_transparent
       Closure.betaiotazeta
-      (Names.Idpred.full,Names.Cpred.complement !predref)
+      (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Pp.msgnl (Printer.pr_goal gl);
+    then Pp.msg_debug (Printer.pr_goal gl);
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
@@ -120,5 +119,6 @@ let ground_tac solver startseq gl=
 		  end
 	    with Heap.EmptyHeap->solver
       end gl in
-    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
+    let seq, gl' = startseq gl in
+    wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
 
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 380326e7..5b320786 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,11 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 val ground_tac:     Tacmach.tactic ->
-  (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+  (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index d45ab0c3..a88778c7 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,28 +1,27 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Formula
-open Sequent
 open Unify
 open Rules
+open Errors
 open Util
 open Term
+open Vars
 open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
 open Termops
 open Reductionops
-open Declarations
 open Formula
 open Sequent
 open Names
-open Libnames
+open Misctypes
 
 let compare_instance inst1 inst2=
 	match inst1,inst2 with
@@ -30,18 +29,18 @@ let compare_instance inst1 inst2=
 	      (OrderedConstr.compare d1 d2)
 	  | Real((m1,c1),n1),Real((m2,c2),n2)->
 	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
-	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
-	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
+	  | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
+	  | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
 
 let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else Libnames.RefOrdered.compare id1 id2
+    else Globnames.RefOrdered.compare id1 id2
 
 module OrderedInstance=
 struct
-  type t=instance * Libnames.global_reference
+  type t=instance * Globnames.global_reference
   let compare (inst1,id1) (inst2,id2)=
     (compare_instance =? compare_gr) inst2 inst1 id2 id1
     (* we want a __decreasing__ total order *)
@@ -76,7 +75,7 @@ let match_one_quantified_hyp setref seq lf=
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
 	if do_sequent setref triv lf.id seq i dom lf.atoms then
 	  setref:=IS.add ((Phantom dom),lf.id) !setref
-    | _ ->anomaly "can't happen"
+    | _ -> anomaly (Pp.str "can't happen")
 
 let give_instances lf seq=
   let setref=ref IS.empty in
@@ -99,36 +98,36 @@ let rec collect_quantified seq=
 
 let dummy_constr=mkMeta (-1)
 
-let dummy_bvid=id_of_string "x"
+let dummy_bvid=Id.of_string "x"
 
-let mk_open_instance id gl m t=
+let mk_open_instance id idc gl m t=
   let env=pf_env gl in
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl (constr_of_global id) in
+      let typ=pf_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
-  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
+  let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   let rec aux n avoid=
-    if n=0 then [] else
+    if Int.equal n 0 then [] else
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] nt in
+  let rawt=Detyping.detype false [] env evmap nt in
   let rec raux n t=
-    if n=0 then t else
+    if Int.equal n 0 then t else
       match t with
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1)
-	| _-> anomaly "can't happen" in
+	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
+	| _-> anomaly (Pp.str "can't happen") in
   let ntt=try
-    Pretyping.Default.understand evmap env (raux m rawt)
+    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
   with e when Errors.noncritical e ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
@@ -141,50 +140,53 @@ let left_instance_tac (inst,id) continue seq=
 	if lookup (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (cut dom)
+	  tclTHENS (Proofview.V82.of_tactic (cut dom))
 	    [tclTHENLIST
-	       [introf;
+	       [Proofview.V82.of_tactic introf;
+                pf_constr_of_global id (fun idc ->
 		(fun gls->generalize
-		   [mkApp(constr_of_global id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		introf;
+		   [mkApp(idc,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
-	    tclTRY assumption]
+	    tclTRY (Proofview.V82.of_tactic assumption)]
     | Real((m,t) as c,_)->
 	if lookup (id,Some c) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
 	  let special_generalize=
 	    if m>0 then
-	      fun gl->
-		let (rc,ot)= mk_open_instance id gl m t in
-		let gt=
-		  it_mkLambda_or_LetIn
-		    (mkApp(constr_of_global id,[|ot|])) rc in
-		  generalize [gt] gl
+	      pf_constr_of_global id (fun idc ->
+		fun gl->
+		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let gt=
+		    it_mkLambda_or_LetIn
+		      (mkApp(idc,[|ot|])) rc in
+		    generalize [gt] gl)
 	    else
-	      generalize [mkApp(constr_of_global id,[|t|])]
+	      pf_constr_of_global id (fun idc ->
+		generalize [mkApp(idc,[|t|])])
 	  in
 	    tclTHENLIST
 	      [special_generalize;
-	       introf;
+	       Proofview.V82.of_tactic introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
 
 let right_instance_tac inst continue seq=
   match inst with
       Phantom dom ->
-	tclTHENS (cut dom)
+	tclTHENS (Proofview.V82.of_tactic (cut dom))
 	[tclTHENLIST
-	   [introf;
+	   [Proofview.V82.of_tactic introf;
 	    (fun gls->
-	       split (Glob_term.ImplicitBindings
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	       Proofview.V82.of_tactic (split (ImplicitBindings
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY assumption]
+	 tclTRY (Proofview.V82.of_tactic assumption)]
     | Real ((0,t),_) ->
-	(tclTHEN (split (Glob_term.ImplicitBindings [t]))
+	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 709eb96f..2f69ad7b 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -1,15 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open Tacmach
-open Names
-open Libnames
+open Globnames
 open Rules
 
 val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b043ba5f..382d5409 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,22 +1,24 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
+open Vars
 open Tacmach
 open Tactics
 open Tacticals
 open Termops
-open Declarations
 open Formula
 open Sequent
-open Libnames
+open Globnames
+open Locus
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -25,13 +27,13 @@ type lseqtac= global_reference -> seqtac
 type 'a with_backtracking = tactic -> 'a
 
 let wrap n b continue seq gls=
-  check_for_interrupt ();
+  Control.check_for_interrupt ();
   let nc=pf_hyps gls in
   let env=pf_env gls in
   let rec aux i nc ctx=
     if i<=0 then seq else
       match nc with
-	  []->anomaly "Not the expected number of hyps"
+	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| ((id,_,typ) as nd)::q->
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
@@ -51,38 +53,38 @@ let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
 
-
 (* connection rules *)
 
 let axiom_tac t seq=
-  try exact_no_check (constr_of_global (find_left t seq))
+  try pf_constr_of_global (find_left t seq) exact_no_check
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
   tclIFTHENELSE
     (try
       tclTHENLIST
-	[generalize [mkApp(constr_of_global id,
-			   [|constr_of_global (find_left a seq)|])];
+	[pf_constr_of_global (find_left a seq) (fun left ->
+	  pf_constr_of_global id (fun id -> 
+	    generalize [mkApp(id, [|left|])]));
 	 clear_global id;
-	 intro]
+	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
     (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
 
 let and_tac backtrack continue seq=
-  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
+  tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack
 
 let or_tac backtrack continue seq=
   tclORELSE
-    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
+    (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq))))))
     backtrack
 
 let arrow_tac backtrack continue seq=
-  tclIFTHENELSE intro (wrap 1 true continue seq)
+  tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq)
     (tclORELSE
-       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
+       (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq)))
        backtrack)
 (* left connectives rules *)
 
@@ -90,9 +92,9 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [simplest_elim (constr_of_global id);
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
        clear_global id;
-       tclDO n intro])
+       tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
      backtrack gls
 
@@ -101,59 +103,58 @@ let left_or_tac ind backtrack id continue seq gls=
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n intro;
+       tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (simplest_elim (constr_of_global id))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  simplest_elim (constr_of_global id)
+  Proofview.V82.of_tactic (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 largs backtrack id continue seq gl=
-     let rcs=ind_hyps 0 ind largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
+     let rcs=ind_hyps 0 indu largs gl in
      let vargs=Array.of_list largs in
-	     (* construire le terme  H->B, le generaliser etc *)
-     let myterm i=
+             (* construire le terme  H->B, le generaliser etc *)
+     let myterm idc i=
        let rc=rcs.(i) in
        let p=List.length rc in
-       let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) 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 (constr_of_global id)),[|capply|]) in
-	 it_mkLambda_or_LetIn head rc in
+       let head=mkApp ((lift p idc),[|capply|]) in
+         it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps=list_tabulate myterm lp in
+       let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [generalize newhyps;
+	      [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
 	       clear_global id;
-	       tclDO lp intro])
+	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_global id),
-			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+  let d idc =mkLambda (Anonymous,b,
+		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (cut c)
+      (tclTHENS (Proofview.V82.of_tactic (cut c))
 	 [tclTHENLIST
-	    [introf;
+	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (cut cc)
-            [exact_no_check (constr_of_global id);
+	  tclTHENS (Proofview.V82.of_tactic (cut cc))
+            [pf_constr_of_global id exact_no_check;
 	     tclTHENLIST
-	       [generalize [d];
+	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
 		clear_global id;
-		introf;
-		introf;
+		Proofview.V82.of_tactic introf;
+		Proofview.V82.of_tactic introf;
 		tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
@@ -161,9 +162,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 
 let forall_tac backtrack continue seq=
   tclORELSE
-    (tclIFTHENELSE intro (wrap 0 true continue seq)
+    (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq)
        (tclORELSE
-	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+	  (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
@@ -173,24 +174,25 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (simplest_elim (constr_of_global id))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (tclTHENLIST [clear_global id;
-                    tclDO n intro;
+                    tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
       backtrack
       gls
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
-    (tclTHENS (cut prod)
+    (tclTHENS (Proofview.V82.of_tactic (cut prod))
        [tclTHENLIST
-	  [intro;
+	  [Proofview.V82.of_tactic intro;
+           pf_constr_of_global id (fun idc ->
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
-	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls);
+              let term=mkApp(idc,[|mkVar(id0)|]) in
+		tclTHEN (generalize [term]) (clear [id0]) gls));
 	   clear_global id;
-	   intro;
+	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
 	tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
@@ -202,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [all_occurrences,EvalConstRef (destConst (constant "not"));
-   all_occurrences,EvalConstRef (destConst (constant "iff"))]
+  [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
 
 let normalize_evaluables=
   onAllHypsAndConcl
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index d5fe398f..596e8535 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,7 +9,7 @@
 open Term
 open Tacmach
 open Names
-open Libnames
+open Globnames
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -19,7 +19,7 @@ type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val basename_of_global: global_reference -> identifier
+val basename_of_global: global_reference -> Id.t
 
 val clear_global: global_reference -> tactic
 
@@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking
 
 val arrow_tac : seqtac with_backtracking
 
-val left_and_tac : inductive -> lseqtac with_backtracking
+val left_and_tac : pinductive -> lseqtac with_backtracking
 
-val left_or_tac : inductive -> lseqtac with_backtracking
+val left_or_tac : pinductive -> lseqtac with_backtracking
 
 val left_false_tac : global_reference -> tactic
 
-val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
+val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking
 
 val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
 
 val forall_tac : seqtac with_backtracking
 
-val left_exists_tac : inductive -> lseqtac with_backtracking
+val left_exists_tac : pinductive -> lseqtac with_backtracking
 
 val ll_forall_tac : types -> lseqtac with_backtracking
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 50cf14a9..2f7f21e4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,18 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Formula
 open Unify
 open Tacmach
-open Names
-open Libnames
+open Globnames
 open Pp
 
 let newcnt ()=
@@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 		| LLexists (_,_)   ->  50
 		| LLarrow  (_,_,_) -> -10
 
-let left_reversible lpat=(priority lpat)>0
-
 module OrderedFormula=
 struct
   type t=Formula.t
@@ -69,12 +67,14 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Libnames.RefOrdered.compare
-     =? (fun oc1 oc2 ->
-	   match oc1,oc2 with
-	       Some (m1,c1),Some (m2,c2) ->
-		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
-	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
+    let c = Globnames.RefOrdered.compare id1 id2 in
+    if c = 0 then
+      let cmp (i1, c1) (i2, c2) =
+        let c = Int.compare i1 i2 in
+        if c = 0 then OrderedConstr.compare c1 c2 else c
+      in
+      Option.compare cmp co1 co2
+    else c
 end
 
 module CM=Map.Make(OrderedConstr)
@@ -90,7 +90,7 @@ let cm_add typ nam cm=
 let cm_remove typ nam cm=
   try
     let l=CM.find typ cm in
-    let l0=List.filter (fun id->id<>nam) l in
+    let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
       match l0 with
 	  []->CM.remove typ cm
 	| _ ->CM.add typ l0 cm
@@ -120,10 +120,10 @@ let lookup item seq=
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
+	    | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in
 	  History.exists p seq.history
 
-let rec add_formula side nam t seq gl=
+let add_formula side nam t seq gl=
   match build_formula side nam t gl seq.cnt with
       Left f->
 	begin
@@ -163,8 +163,6 @@ let find_left t seq=List.hd (CM.find t seq.context)
       left_reversible lpat
   with Heap.EmptyHeap -> false
 *)
-let no_formula seq=
-  seq.redexes=HP.empty
 
 let rec take_formula seq=
   let hd=HP.maximum seq.redexes
@@ -191,36 +189,36 @@ let empty_seq depth=
    depth=depth}
 
 let expand_constructor_hints =
-  list_map_append (function
+  List.map_append (function
     | IndRef ind ->
-	list_tabulate (fun i -> ConstructRef (ind,i+1))
-	  (Inductiveops.nconstructors ind)
+        List.init (Inductiveops.nconstructors ind)
+          (fun i -> ConstructRef (ind,i+1))
     | gr ->
 	[gr])
 
-let extend_with_ref_list l seq gl=
+let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
-  let f gr seq=
-    let c=constr_of_global gr in
+  let f gr (seq,gl) =
+    let gl, c = pf_eapply Evd.fresh_global gl gr in
     let typ=(pf_type_of gl c) in
-      add_formula Hyp gr typ seq gl in
-    List.fold_right f l seq
+      (add_formula Hyp gr typ seq gl,gl) in
+    List.fold_right f l (seq,gl)
 
-open Auto
+open Hints
 
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
     match p_a_t.code with
-	Res_pf (c,_) | Give_exact c
+	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
-	     let gr=global_of_constr c in
+	     let gr = global_of_constr c in
 	     let typ=(pf_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-  let g _ l = List.iter f l in
+  let g _ _ l = List.iter f l in
   let h dbname=
     let hdb=
       try
@@ -229,18 +227,18 @@ 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
+    !seqref, gl (*FIXME: forgetting about universes*)
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) c in
+    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in
       str "| " ++
-      Util.prlist Printer.pr_global l ++
+      prlist Printer.pr_global l ++
       str " : " ++
       Ppconstr.pr_constr_expr xc ++
       cut () ++
       s in
-    msgnl (v 0
+    (v 0
 	     (str "-----" ++
 	      cut () ++
 	      CM.fold print_entry map (mt ()) ++
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 44b5ed3e..dc3f05be 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,17 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Term
-open Util
 open Formula
 open Tacmach
-open Names
-open Libnames
+open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=constr
 
@@ -56,9 +54,9 @@ val take_formula : t -> Formula.t * t
 val empty_seq : int -> t
 
 val extend_with_ref_list : global_reference list ->
-  t -> Proof_type.goal sigma -> t
+  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
 
-val extend_with_auto_hints : Auto.hint_db_name list ->
-  t -> Proof_type.goal sigma -> t
+val extend_with_auto_hints : Hints.hint_db_name list ->
+  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
 
-val print_cmap: global_reference list CM.t -> unit
+val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 00eb9981..0a172034 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,16 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Util
-open Formula
-open Tacmach
 open Term
-open Names
+open Vars
 open Termops
 open Reductionops
 
@@ -34,7 +32,7 @@ let unif t1 t2=
     match kind_of_term t with
 	Meta i->
 	  (try
-	     head_reduce (List.assoc i !sigma)
+	     head_reduce (Int.List.assoc i !sigma)
 	   with Not_found->t)
       | _->t in
     Queue.add (t1,t2) bige;
@@ -44,17 +42,17 @@ let unif t1 t2=
       and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
-	      if i<>j then
+	      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 Intset.is_empty (free_rels t) &&
+		if Int.Set.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Intset.is_empty (free_rels t) &&
+		if Int.Set.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
@@ -65,7 +63,7 @@ let unif t1 t2=
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
 	      let l=Array.length va in
-		if l<>(Array.length vb) then
+		if not (Int.equal l (Array.length vb)) then
 		  raise (UFAIL (nt1,nt2))
 		else
 		  for i=0 to l-1 do
@@ -74,13 +72,13 @@ let unif t1 t2=
 	  | App(ha,va),App(hb,vb)->
 	      Queue.add (ha,hb) bige;
 	      let l=Array.length va in
-		if l<>(Array.length vb) then
+		if not (Int.equal l (Array.length vb)) then
 		  raise (UFAIL (nt1,nt2))
 		else
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
 		  done
-	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
+	  | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
       assert false
 	(* this place is unreachable but needed for the sake of typing *)
@@ -90,7 +88,7 @@ let value 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 && destMeta term = i then 0 else
+    if isMeta term && Int.equal (destMeta term) i then 0 else
       let f v t=add v (vaux t) in
       let vr=fold_constr f (-1) term in
 	if vr<0 then -1 else vr+1 in
@@ -107,7 +105,7 @@ let mk_rel_inst t=
     match kind_of_term t with
 	Meta n->
 	  (try
-	     mkRel (d+(List.assoc n !rel_env))
+	     mkRel (d+(Int.List.assoc n !rel_env))
 	   with Not_found->
 	     let m= !new_rel in
 	       incr new_rel;
@@ -119,7 +117,7 @@ let mk_rel_inst t=
 
 let unif_atoms i dom t1 t2=
   try
-    let t=List.assoc i (unif t1 t2) in
+    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))
   with
@@ -127,7 +125,7 @@ let unif_atoms i dom t1 t2=
     | Not_found ->Some (Phantom dom)
 
 let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+  let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
 let more_general (m1,t1) (m2,t2)=
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 697548be..15318546 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)