Imported Upstream version 8.5~beta3+dfsg

35 files changed, 481 insertions, 488 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index bc5a3900..ee7341a4 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -283,7 +283,7 @@ end.
 
 (** Quotienting a polynomial by the relation X_i^2 ~ X_i *)
 
-(* Remove the multiple occurences of monomials x_k *)
+(* Remove the multiple occurrences of monomials x_k *)
 
 Fixpoint reduce_aux k p :=
 match p with
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 29bca862..97ea5fdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -129,14 +129,14 @@ type cinfo=
      ci_nhyps: int}     (* # projectable args *)
 
 let family_eq f1 f2 = match f1, f2 with
-| InProp, InProp
-| InSet, InSet
-| InType, InType -> true
-| _ -> false
+  | Prop Pos, Prop Pos
+  | Prop Null, Prop Null
+  | Type _, Type _ -> true
+  | _ -> false
 
 type term=
     Symb of constr
-  | Product of sorts_family * sorts_family
+  | Product of sorts * sorts
   | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
@@ -161,7 +161,7 @@ let hash_sorts_family = function
 
 let rec hash_term = function
   | Symb c -> combine 1 (hash_constr c)
-  | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
+  | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
   | Eps i -> combine 3 (Id.hash i)
   | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
   | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
@@ -425,8 +425,8 @@ let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
-  mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
-	   mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
+  mkLambda(_A_,mkSort(s1),
+	   mkLambda(_B_,mkSort(s2),_body_))
 
 let rec constr_of_term = function
     Symb s-> applist_projection s []
@@ -513,7 +513,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls trm in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -836,7 +836,7 @@ let complete_one_class state i=
 	    let _,etyp,rest= destProd typ in
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-	let _c = pf_type_of state.gls
+	let _c = pf_unsafe_type_of state.gls
 	  (constr_of_term (term state.uf pac.cnode)) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c72843d5..0dcf3a87 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -30,7 +30,7 @@ type cinfo =
 
 type term =
     Symb of constr
-  | Product of sorts_family * sorts_family
+  | Product of sorts * sorts
   | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1..068cb25c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -46,7 +46,7 @@ let whd_delta env=
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c)
+let sf_of env sigma c = sort_of env (ref sigma) c
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -253,9 +253,15 @@ let new_app_global f args k =
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
+let assert_before n c =
+  Proofview.Goal.enter begin fun gl ->
+    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+      Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
+  end
+    
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of t = Tacmach.New.pf_type_of gl t in
+  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check c
@@ -302,9 +308,9 @@ let rec proof_tac p : unit Proofview.tactic =
   	     Tacticals.New.tclFIRST
 	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-                Proofview.tclZERO (UserError ("Congruence" ,
+                Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")))]]
+		       "I don't know how to handle dependent equality")]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
@@ -325,7 +331,7 @@ let refute_tac c t1 t2 p =
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
   in
   let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
@@ -335,14 +341,14 @@ let refute_tac c t1 t2 p =
   end
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply e_type_of gl c in
+  let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
   in
   let neweq= new_app_global _eq [|sort;tt1;tt2|] in
   let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
@@ -367,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.nf_enter begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
+      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
     in
     let concl = Proofview.Goal.concl gl in
     (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
@@ -376,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p =
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_type_of gls identity in *)
+    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
@@ -476,19 +482,28 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
-
+    
+let mk_eq f c1 c2 k =
+  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+  Proofview.Goal.enter begin
+    fun gl ->
+    let open Tacmach.New in
+    let evm, ty = pf_apply type_of gl c1 in
+    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
+    let term = mkApp (fc, [| ty; c1; c2 |]) in
+    let evm, _ =  type_of (pf_env gl) evm term in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
+			  (k term)
+    end)
+    
 let f_equal =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let type_of = Tacmach.New.pf_type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
-        let ty = (* Termops.refresh_universes *) (type_of c1) in
-        if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
-        else
-          Tacticals.New.tclTRY (Tacticals.New.tclTHEN
-          ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
-          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+        Tacticals.New.tclTHEN
+	  (mk_eq _eq c1 c2 Tactics.cut)
+	  (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d0b7f34..1a908064 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -125,10 +125,34 @@ let go_to_proof_mode () =
 
 (* closing gaps *)
 
+(* spiwack: should use [Proofview.give_up] but that would require
+   moving the whole declarative mode into the new proof engine.  It
+   will eventually have to be done.
+
+   As far as I can tell, [daimon_tac] is used after a [thus thesis],
+   it will leave uninstantiated variables instead of giving a relevant
+   message at [Qed]. *)
 let daimon_tac gls =
   set_daimon_flag ();
   {it=[];sigma=sig_sig gls;}
 
+let daimon_instr env p =
+  let (p,(status,_)) =
+    Proof.run_tactic env begin
+      Proofview.tclINDEPENDENT Proofview.give_up
+    end p
+  in
+  p,status
+
+let do_daimon () =
+  let env = Global.env () in
+  let status =
+    Proof_global.with_current_proof begin fun _ p ->
+      daimon_instr env p
+    end
+  in
+  if not status then Pp.feedback Feedback.AddedAxiom else ()
+
 (* post-instruction focus management *)
 
 let goto_current_focus () = 
@@ -144,7 +168,7 @@ let goto_current_focus_or_top () =
 (* return *)
 
 let close_tactic_mode () =
-  try goto_current_focus ()
+  try do_daimon ();goto_current_focus ()
   with Not_found ->
     error "\"return\" cannot be used outside of Declarative Proof Mode."
 
@@ -165,7 +189,7 @@ let close_block bt pts =
       in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
-	  (goto_current_focus ())
+	  do_daimon ();goto_current_focus ()
       | _, Claim::_ ->
 	  error "\"end claim\" expected."
       | _, Focus_claim::_ ->
@@ -188,7 +212,7 @@ let close_previous_case pts =
     Proof.is_done pts
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
+	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
@@ -196,7 +220,7 @@ let close_previous_case pts =
     match get_stack pts with
 	Per (et,_,_,_) :: _ -> ()
       | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus ()
+	  do_daimon ();goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
 
 (* Proof instructions *)
@@ -749,7 +773,7 @@ let rec take_tac wits gls =
   match wits with
       [] -> tclIDTAC gls
     | wit::rest ->
-	let typ = pf_type_of gls wit in
+	let typ = pf_unsafe_type_of gls wit in
 	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
@@ -830,7 +854,7 @@ let start_tree env ind rp =
 let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
-  let ctyp=pf_type_of gls casee in
+  let ctyp=pf_unsafe_type_of gls casee in
   let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
   let (ind,u) =
@@ -845,7 +869,7 @@ let build_per_info etype casee gls =
       | _ -> mind.mind_nparams,None in
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
-    let typ=pf_type_of gls c in
+    let typ=pf_unsafe_type_of gls c in
       lambda_create env (typ,subst_term c body) in
   let pred= List.fold_right abstract_obj
     real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1204,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let nparams = mind.mind_nparams in
 	let concl=pf_concl gls in
 	let env=pf_env gls in
-	let ctyp=pf_type_of gls casee in
+	let ctyp=pf_unsafe_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
-	  let typ=pf_type_of gls c in
+	  let typ=pf_unsafe_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in
 	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31..d6c29283 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body)
-    : Entries.const_entry_body =
+let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
+    : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
   end
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index fbcd01a1..cf97ae3a 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with.
 in extracted code. 
 
 
-* A few constants are explicitely declared to be inlined in extracted code. 
+* A few constants are explicitly declared to be inlined in extracted code.
 For the moment there are: 
 	Wf.Acc_rec
 	Wf.Acc_rect
@@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not.
 
 Print Extraction Inline. 
 
-Sum up the current state of the table recording the custom inlings 
+Sum up the current state of the table recording the custom inlinings
 (Extraction (No)Inline). 
 
 Reset Extraction Inline. 
 
-Put the table recording the custom inlings back to empty. 
+Put the table recording the custom inlinings back to empty.
 
 As a consequence, there is no more need for options inside the commands of 
 extraction: 
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
new file mode 100644
index 00000000..e94e7d42
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Int] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
new file mode 100644
index 00000000..038f0ed8
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Integer] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Integer] isn't necessarily a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
new file mode 100644
index 00000000..244eb85f
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -0,0 +1,35 @@
+(**
+ * Efficient (but uncertified) extraction of usual [nat] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances.  Useful in combination with
+ * [Extract Inductive nat] that maps [nat] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import Arith.
+Require Import EqNat.
+
+Extract Inlined Constant Nat.add => "(Prelude.+)".
+Extract Inlined Constant Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Nat.max => "Prelude.max".
+Extract Inlined Constant Nat.min => "Prelude.min".
+Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
+Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Init.Nat.max => "Prelude.max".
+Extract Inlined Constant Init.Nat.min => "Prelude.min".
+Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
+Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
+Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
+Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
+Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
+Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
+
+Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+
+Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
new file mode 100644
index 00000000..3558f4f2
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -0,0 +1,38 @@
+(**
+ * Special handling of ascii and strings for extraction to Haskell.
+ *)
+
+Require Import Ascii.
+Require Import String.
+
+(**
+ * At the moment, Coq's extraction has no way to add extra import
+ * statements to the extracted Haskell code.  You will have to
+ * manually add:
+ *
+ *   import qualified Data.Bits
+ *   import qualified Data.Char
+ *)
+
+Extract Inductive ascii => "Prelude.Char"
+  [ "(\b0 b1 b2 b3 b4 b5 b6 b7 -> Data.Char.chr (
+      (if b0 then Data.Bits.shiftL 1 0 else 0) Prelude.+
+      (if b1 then Data.Bits.shiftL 1 1 else 0) Prelude.+
+      (if b2 then Data.Bits.shiftL 1 2 else 0) Prelude.+
+      (if b3 then Data.Bits.shiftL 1 3 else 0) Prelude.+
+      (if b4 then Data.Bits.shiftL 1 4 else 0) Prelude.+
+      (if b5 then Data.Bits.shiftL 1 5 else 0) Prelude.+
+      (if b6 then Data.Bits.shiftL 1 6 else 0) Prelude.+
+      (if b7 then Data.Bits.shiftL 1 7 else 0)))" ]
+  "(\f a -> f (Data.Bits.testBit (Data.Char.ord a) 0)
+              (Data.Bits.testBit (Data.Char.ord a) 1)
+              (Data.Bits.testBit (Data.Char.ord a) 2)
+              (Data.Bits.testBit (Data.Char.ord a) 3)
+              (Data.Bits.testBit (Data.Char.ord a) 4)
+              (Data.Bits.testBit (Data.Char.ord a) 5)
+              (Data.Bits.testBit (Data.Char.ord a) 6)
+              (Data.Bits.testBit (Data.Char.ord a) 7))".
+Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+
+Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
+Extract Inlined Constant String.string_dec => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
new file mode 100644
index 00000000..66690851
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -0,0 +1,24 @@
+(** Extraction of [Z] into Haskell's [Int] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [Z] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive positive => "Prelude.Int" [
+  "(\x -> 2 Prelude.* x Prelude.+ 1)"
+  "(\x -> 2 Prelude.* x)"
+  "1" ]
+  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+                   if Prelude.odd n
+                   then fI (n `Prelude.div` 2)
+                   else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Int" [ "0" "(\x -> x)" "Prelude.negate" ]
+  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+                   if n Prelude.> 0 then fP n else
+                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
new file mode 100644
index 00000000..f192f16e
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -0,0 +1,23 @@
+(** Extraction of [Z] into Haskell's [Integer] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [Z] into [Integer] isn't necessarily a good idea.
+    See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive positive => "Prelude.Integer" [
+  "(\x -> 2 Prelude.* x Prelude.+ 1)"
+  "(\x -> 2 Prelude.* x)"
+  "1" ]
+  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+                   if Prelude.odd n
+                   then fI (n `Prelude.div` 2)
+                   else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ]
+  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+                   if n Prelude.> 0 then fP n else
+                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
new file mode 100644
index 00000000..cbbfda75
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -0,0 +1,21 @@
+(**
+ * Efficient (but uncertified) extraction of usual [Z] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances.  Useful in combination with
+ * [Extract Inductive Z] that maps [Z] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import ZArith.
+Require Import EqNat.
+
+Extract Inlined Constant Z.add => "(Prelude.+)".
+Extract Inlined Constant Z.sub => "(Prelude.-)".
+Extract Inlined Constant Z.mul => "(Prelude.*)".
+Extract Inlined Constant Z.max => "Prelude.max".
+Extract Inlined Constant Z.min => "Prelude.min".
+Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)".
+Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)".
+
+Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 080512b2..6ae519ef 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args =
     | Construct (cp,u) ->
 	extract_cons_app env mle mlt cp u args
     | Proj (p, c) ->
-        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
+        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+	  extract_term env mle mlt term args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9fdb0205..6fc1195f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
-   occurences in different branches aren't added, but we rather use max. *)
+(* Number of occurrences of [Rel 1] in [t], with special treatment of match:
+   occurrences in different branches aren't added, but we rather use max. *)
 
 let nb_occur_match =
   let rec nb k = function
@@ -851,7 +851,7 @@ let factor_branches o typ br =
     else Some (br_factor, br_set)
   end
 
-(*s If all branches are functions, try to permut the case and the functions. *)
+(*s If all branches are functions, try to permute the case and the functions. *)
 
 let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
@@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
   purge the args of [MLrel r] corresponding to a [dummy_name].
   It makes eta-expansion if needed. *)
 
@@ -1351,10 +1351,10 @@ let is_not_strict t =
    We expand small terms with at least one non-strict
    variable (i.e. a variable that may not be evaluated).
 
-   Futhermore we don't expand fixpoints.
+   Furthermore we don't expand fixpoints.
 
-   Moreover, as mentionned by X. Leroy (bug #2241),
-   inling a constant from inside an opaque module might
+   Moreover, as mentioned by X. Leroy (bug #2241),
+   inlining a constant from inside an opaque module might
    break types. To avoid that, we require below that
    both [r] and its body are globally visible. This isn't
    fully satisfactory, since [r] might not be visible (functor),
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f0489048..9c30c5eb 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,11 @@
 ExtrHaskellBasic.vo
+ExtrHaskellNatNum.vo
+ExtrHaskellNatInt.vo
+ExtrHaskellNatInteger.vo
+ExtrHaskellZNum.vo
+ExtrHaskellZInt.vo
+ExtrHaskellZInteger.vo
+ExtrHaskellString.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
@@ -6,4 +13,4 @@ ExtrOcamlNatInt.vo
 ExtrOcamlNatBigInt.vo
 ExtrOcamlZInt.vo
 ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo
\ No newline at end of file
+ExtrOcamlString.vo
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5912f0a0..c80a8081 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl idc in
+      let typ=pf_unsafe_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
@@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
-		    try Typing.e_type_of (pf_env gl) evmap gt
+		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when Errors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7d034db5..a77af03d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
   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_type_of gl c) in
+    let typ=(pf_unsafe_type_of gl c) in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -209,12 +209,13 @@ open Hints
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
-    match repr_auto_tactic p_a_t.code with
+    match repr_hint p_a_t.code with
 	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
+          let (c, _, _) = c in
 	  (try
 	     let gr = global_of_constr c in
-	     let typ=(pf_type_of gl c) in
+	     let typ=(pf_unsafe_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4a832435..169a7060 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   let evm, _ = pf_apply Typing.e_type_of g to_refine in
+	   let evm, _ = pf_apply Typing.type_of g to_refine in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
@@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
+	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
 	   (* compute the new value of the body *)
 	   let new_term_value =
 	     match kind_of_term new_term_value_eq with
@@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
-		    pf_type_of g' term,
+		    pf_unsafe_type_of g' term,
 		    Termops.replace_term term (mkRel 1) dyn_infos.info
 		   )
 	 in
@@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let evm, _ = pf_apply Typing.e_type_of g c in
+	  let evm, _ = pf_apply Typing.type_of g c in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -699,7 +699,7 @@ let build_proof
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
 		  let g_nb_prod = nb_prod (pf_concl g) in
-		  let type_of_term = pf_type_of g t in
+		  let type_of_term = pf_unsafe_type_of g t in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
@@ -919,7 +919,7 @@ let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
   let env = Global.env () in
-  let hyp_typ = pf_type_of g (mkVar hyp) in
+  let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
   let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if Id.List.mem hyp hyps
@@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
-    let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f
+    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
     in 
     decompose_prod_n_assum
       (nb_params + nb_args) t,evd
@@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Global.env ()) !evd
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
-      let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in 
-      evd:=evd';		       
+      evd:=evd';                       
+      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
@@ -1414,7 +1414,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
-    let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in
+    let _,hrec_concl  = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
     let f_app = Array.last (snd (destApp hrec_concl)) in
     let f =  (fst (destApp f_app)) in
     let rec backtrack : tactic =
@@ -1641,7 +1641,7 @@ let prove_principle_for_gen
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
       (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1));
-(*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
+(*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf5..c47602bd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
-  let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
+  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -303,7 +303,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   try
 
   let f = funs.(i) in
-  let type_sort = Universes.new_sort_in_family InType in
+  let env = Global.env () in    
+  let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
   let new_sorts =
     match sorts with
       | None -> Array.make (Array.length funs) (type_sort)
@@ -317,23 +318,23 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let names = ref [new_princ_name] in
-  let evd' = !evd in 
   let hook =
     fun  new_principle_type _ _  -> 
     if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
-	let s = Universes.new_sort_in_family fam_sort in
+	let evd' = Evd.from_env (Global.env ()) in
+	let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
 	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
+	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
 	ignore(
 	  Declare.declare_constant
 	    name
-	    (Entries.DefinitionEntry ce,
+	    (DefinitionEntry ce,
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme))
 	);
 	Declare.definition_message name;
@@ -394,7 +395,7 @@ let get_funs_constant mp dp =
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	      (Global.env ())
-	      (Evd.empty)
+	      (Evd.from_env (Global.env ()))
 	      body
 	    in
 	    body
@@ -446,7 +447,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -478,16 +479,15 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (Typing.type_of env sigma) schemes
+    List.map (Typing.unsafe_type_of env sigma) schemes
   in
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
 	     )
       fas
   in
-  evd:=sigma;
   (* We create the first priciple by tactic *)
   let first_type,other_princ_types =
     match l_schemes with
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+    let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
     let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
@@ -585,30 +585,29 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
 	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
-	      Entries.const_entry_body = 
-                (Future.from_val (Term_typing.mk_pure_proof princ_body));
-	      Entries.const_entry_type = Some scheme_type
+	      const_entry_body = 
+                (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+	      const_entry_type = Some scheme_type
 	   }
       )
       other_fun_princ_types
     in
     const::other_result
 
-	   
 let build_scheme fas =
-  Dumpglob.pause ();
-  let evd = (ref Evd.empty) in
+  let evd = (ref (Evd.from_env (Global.env ()))) in
   let pconstants = (List.map
 	 (fun (_,f,sort) ->
 	    let f_as_constant =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+                errorlabstrm "FunInd.build_scheme"
+                  (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
-	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
-	    let _ = evd := evd' in 
+            let _ = evd := evd' in 
+	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in 
 	    (destConst f,sort)
 	 )
 	 fas
@@ -621,25 +620,24 @@ let build_scheme fas =
        ignore
 	 (Declare.declare_constant
 	    princ_id
-	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+	    (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
        Declare.definition_message princ_id
     )
     fas
-    bodies_types;
-    Dumpglob.continue ()
-
-
+    bodies_types
 
 let build_case_scheme fa =
   let env = Global.env ()
-  and sigma = Evd.empty in
+  and sigma = (Evd.from_env (Global.env ())) in
 (*   let id_to_constr id =  *)
 (*     Constrintern.global_reference  id *)
 (*   in  *)
-  let funs =  (fun (_,f,_) ->
-		 try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
-		 with Not_found ->
-		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+  let funs =
+    let (_,f,_) = fa in
+    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    with Not_found ->
+      errorlabstrm "FunInd.build_case_scheme"
+        (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -656,7 +654,7 @@ let build_case_scheme fa =
   in
   let sigma, scheme = 
     (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun in
-  let scheme_type =  (Typing.type_of env sigma ) scheme in
+  let scheme_type =  (Typing.unsafe_type_of env sigma ) scheme in
   let sorts =
     (fun (_,_,x) ->
        Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
@@ -670,14 +668,14 @@ let build_case_scheme fa =
 	    );
   *)
     generate_functional_principle
-      (ref Evd.empty)
+      (ref (Evd.from_env (Global.env ())))
       false
       scheme_type
       (Some ([|sorts|]))
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|])
+      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
   in
   ()
  
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index f6e5578d..bc082f07 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <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 Names
 open Term
 open Misctypes
@@ -29,7 +37,7 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Entries.definition_entry list
+ (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
 
 val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
 val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 043d4328..045beb37 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -247,247 +247,3 @@ END
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 ["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
 END
-
-
-
-
-
-(* FINDUCTION *)
-
-(* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
-  (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-let prNamedConstr s c =
-  begin
-    msg(str "");
-    msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
-    msg(str "");
-  end
-
-
-
-(** Information about an occurrence of a function call (application)
-    inside a term. *)
-type fapp_info = {
-  fname: constr; (** The function applied *)
-  largs: constr list; (** List of arguments *)
-  free: bool; (** [true] if all arguments are debruijn free *)
-  max_rel: int; (** max debruijn index in the funcall *)
-  onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
-}
-
-
-(** [constr_head_match(a b c) a] returns true, false otherwise. *)
-let constr_head_match u t=
-  if isApp u
-  then
-    let uhd,args= destApp u in
-    Constr.equal uhd t
-  else false
-
-(** [hdMatchSub inu t] returns the list of occurrences of [t] in
-    [inu]. DeBruijn are not pushed, so some of them may be unbound in
-    the result. *)
-let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
-  let subres =
-    match kind_of_term inu with
-      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
-	  hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
-      | Fix (_,(lna,tl,bl))  -> (* not sure Fix is correct *)
-	  Array.fold_left
-	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
-	    [] bl
-      | _ -> (* Cofix will be wrong *)
-	  fold_constr
-	    (fun l cstr ->
-	      l @ hdMatchSub cstr test) [] inu in
-  if not (test inu) then subres
-  else
-    let f,args = decompose_app inu in
-    let freeset = Termops.free_rels inu in
-    let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in
-    {fname = f; largs = args; free = Int.Set.is_empty freeset;
-    max_rel = max_rel; onlyvars = List.for_all isVar args }
-    ::subres
-
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkEq typ c1 c2 =
-  mkApp (make_eq(),[| typ; c1; c2|])
-
-
-let poseq_unsafe idunsafe cstr gl =
-  let typ = Tacmach.pf_type_of gl cstr in
-  tclTHEN
-    (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
-    (tclTHENFIRST
-      (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr)))
-      (Proofview.V82.of_tactic Tactics.reflexivity))
-    gl
-
-
-let poseq id cstr gl =
-  let x = Tactics.fresh_id [] id gl in
-  poseq_unsafe x cstr gl
-
-(* dirty? *)
-
-let list_constr_largs = ref []
-
-let rec poseq_list_ids_rec lcstr gl =
-  match lcstr with
-    | [] -> tclIDTAC gl
-    | c::lcstr' ->
-	match kind_of_term c with
-	  | Var _ ->
-	      (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
-	  | _ ->
-	      let _ = prstr "c = " in
-	      let _ = prconstr c in
-	      let _ = prstr "\n" in
-	      let typ = Tacmach.pf_type_of gl c in
-	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
-	      let x = Tactics.fresh_id [] cname gl in
-	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
-	      let _ = prstr " list_constr_largs = " in
-	      let _ = prlistconstr !list_constr_largs in
-	      let _ = prstr "\n" in
-
-	      tclTHEN
-		(poseq_unsafe x c)
-		(poseq_list_ids_rec lcstr')
-		gl
-
-let poseq_list_ids lcstr gl =
-  let _ = list_constr_largs := [] in
-  poseq_list_ids_rec lcstr gl
-
-(** [find_fapp test g] returns the list of [app_info] of all calls to
-    functions that satisfy [test] in the conclusion of goal g. Trivial
-    repetition (not modulo conversion) are deleted. *)
-let find_fapp (test:constr -> bool) g : fapp_info list =
-  let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
-  let res =
-    List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
-  (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
-  res)
-
-
-
-(** [finduction id filter g] tries to apply functional induction on
-    an occurence of function [id] in the conclusion of goal [g]. If
-    [id]=[None] then calls to any function are selected. In any case
-    [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
-    (nexttac:Proof_type.tactic) g =
-  let test = match oid with
-    | Some id ->
-       let idref = const_of_id id in
-       (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *)
-       let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in
-	(fun u -> constr_head_match u idconstr) (* select only id *)
-    | None -> (fun u -> isApp u) in (* select calls to any function *)
-  let info_list = find_fapp test g in
-  let ordered_info_list = heuristic info_list in
-  prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
-  if List.is_empty ordered_info_list then Errors.error "function not found in goal\n";
-  let taclist: Proof_type.tactic list =
-    List.map
-      (fun info ->
-	(tclTHEN
-	  (tclTHEN (poseq_list_ids info.largs)
-	    (
-	      fun gl ->
-		  (functional_induction
-		    true (applist (info.fname, List.rev !list_constr_largs))
-		    None None) gl))
-	  nexttac)) ordered_info_list in
-  (* we try each (f t u v) until one does not fail *)
-  (* TODO: try also to mix functional schemes *)
-  tclFIRST taclist g
-
-
-
-
-(** [chose_heuristic oi x] returns the heuristic for reordering
-    (and/or forgetting some elts of) a list of occurrences of
-     function calls infos to chose first with functional induction. *)
-let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
-  match oi with
-    | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
-    | None ->
-	(* Default heuristic: put first occurrences where all arguments
-	   are *bound* (meaning already introduced) variables *)
-	let ordering x y =
-	  if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
-	  else if x.free && x.onlyvars then -1
-	  else if y.free && y.onlyvars then 1
-	  else 0 (* both not pertinent *)
-	in
-	List.sort ordering
-
-
-
-TACTIC EXTEND finduction
-    ["finduction" ident(id) natural_opt(oi)] ->
-      [
-	match oi with
-	  | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0"
-	  | _ ->
-	      let heuristic = chose_heuristic oi in
-	      Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC)
-      ]
-END
-
-
-
-TACTIC EXTEND fauto
-    [ "fauto" tactic(tac)] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac)))
-      ]
-  |
-    [ "fauto" ] ->
-      [
-	let heuristic = chose_heuristic None in
-	Proofview.V82.tactic (finduction None heuristic tclIDTAC)
-      ]
-
-END
-
-
-TACTIC EXTEND poseq
-  [ "poseq" ident(x) constr(c) ] ->
-      [ Proofview.V82.tactic (poseq x c) ]
-END
-
-VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY
-  [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
-END
-
-VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
-  [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
-      "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
-     [
-       let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
-       let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
-	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
-       let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
-       let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
-       let ar1 = List.length (fst (decompose_prod f1type)) in
-       let ar2 = List.length (fst (decompose_prod f2type)) in
-       let _ =
-	 if not (Int.equal ar1 (List.length cl1)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
-       let _ =
-	 if not (Int.equal ar2 (List.length cl2)) then
-	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
-       Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
-     ]
-END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9e3f3986..1b12cd42 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,20 +333,20 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in
-	let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in
+	let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
+	let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
 let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
-    observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty);
+    observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
     match pat with
       | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
       | PatCstr(_,c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
-	    try Inductiveops.find_rectype env Evd.empty typ
+	    try Inductiveops.find_rectype env (Evd.from_env env) typ
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
@@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env =
 	~init:(env,[])
     )
   in
-  observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty);
+  observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
   res
 
 
@@ -393,7 +393,7 @@ let rec pattern_to_term_and_type env typ  = function
 	  constr
       in
       let Inductiveops.IndType(indf,indargs) =
-	try Inductiveops.find_rectype env Evd.empty typ
+	try Inductiveops.find_rectype env (Evd.from_env env) typ
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
+	     (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
 	  )
       in
       let patl_as_term =
@@ -486,9 +486,9 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   a pseudo value "v1 ... vn".
 		   The "value" of this branch is then simply [res]
 		*)
-		let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
-		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
-		let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
+		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
+		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -594,8 +594,8 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	   and combine the two result
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
-	let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
-	let v_type = Typing.type_of env Evd.empty v_as_constr in
+	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
+	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
 	let new_env =
 	  match n with
 	      Anonymous -> env
@@ -610,10 +610,10 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
-	let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
-	let b_typ = Typing.type_of env Evd.empty b_as_constr in
+	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	let (ind,_) =
-	  try Inductiveops.find_inductive env Evd.empty b_typ
+	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
 	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
@@ -642,10 +642,10 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      )
 	      nal
 	  in
-	  let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
-	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
+	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
+	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	  let (ind,_) =
-	    try Inductiveops.find_inductive env Evd.empty b_typ
+	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
 	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
@@ -689,8 +689,8 @@ and build_entry_lc_from_case env funname make_discr
 	in
 	let types =
 	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
-		      Typing.type_of env Evd.empty case_arg_as_constr
+		      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
+		      Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr
 		   ) el
 	in
 	(****** The next works only if the match is not dependent ****)
@@ -737,11 +737,11 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   List.fold_right
 		     (fun id acc ->
 			let typ_of_id =
-			  Typing.type_of env_with_pat_ids Evd.empty (mkVar id)
+			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
-			    env_with_pat_ids Evd.empty typ_of_id
+			    env_with_pat_ids (Evd.from_env env) typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
@@ -785,15 +785,15 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
-		 let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
+		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
-		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
+		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] new_env Evd.empty typ_of_id
+			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -894,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
-			let t',ctx = Pretyping.understand env Evd.empty new_t in
+			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
 			let new_env = Environ.push_rel (n,None,t') env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
@@ -914,7 +914,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try fst (Pretyping.understand env Evd.empty t)(*FIXME*)
+		      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
                       with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
@@ -937,7 +937,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
 		    let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
-		    let ty',ctx = Pretyping.understand env Evd.empty ty in
+		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
 		    let nparam = mib.Declarations.mind_nparams in
@@ -949,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
-				 env Evd.empty
+				 env (Evd.from_env env)
 				 p) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
@@ -959,7 +959,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
-		    let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in
+		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
 		      match kind_of_term eq'_as_constr with
@@ -978,12 +978,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				     | Name id' ->
 					 (id',Detyping.detype false []
 					    env
-                                            Evd.empty
+                                            (Evd.from_env env)
 					    arg)::acc
 				 else if isVar var_as_constr
 				 then (destVar var_as_constr,Detyping.detype false []
 					 env
-                                         Evd.empty
+                                         (Evd.from_env env)
 					 arg)::acc
 				 else acc
 			      )
@@ -1009,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     if is_in_b then b else  replace_var_by_term id rt b
 		    in
 		    let new_env =
-		      let t',ctx = Pretyping.understand env Evd.empty eq' in
+		      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		      Environ.push_rel (n,None,t') env
 		    in
 		    let new_b,id_to_exclude =
@@ -1047,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  else raise Continue
 	      with Continue -> 
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t',ctx = Pretyping.understand env Evd.empty t in
+		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1063,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t',ctx = Pretyping.understand env Evd.empty t in
+		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1082,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
 	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
-	  let t',ctx = Pretyping.understand env Evd.empty t in
+	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 	  match n with
 	    | Name id ->
 		let new_env = Environ.push_rel (n,None,t') env in
@@ -1104,8 +1104,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | GLetIn(_,n,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
-	  let t',ctx = Pretyping.understand env Evd.empty t in
-	  let type_t' = Typing.type_of env Evd.empty t' in
+	  let evd = (Evd.from_env env) in
+	  let t',ctx = Pretyping.understand env evd t in
+	  let evd = Evd.from_ctx ctx in
+	  let type_t' = Typing.unsafe_type_of env evd t' in
 	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1129,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (crossed_types)
 	      depth t
 	  in
-	  let t',ctx = Pretyping.understand env Evd.empty new_t in
+	  let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
 	  let new_env = Environ.push_rel (na,None,t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1255,7 +1257,7 @@ let do_build_inductive
   let evd,env =
     Array.fold_right2
       (fun id c (evd,env) ->
-       let evd,t = Typing.e_type_of env evd (mkConstU c) in
+       let evd,t = Typing.type_of env evd (mkConstU c) in
        evd,
        Environ.push_named (id,None,t)
 			   (* try *)
@@ -1297,7 +1299,7 @@ let do_build_inductive
     let rel_arities = Array.mapi rel_arity funsargs in
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
 			     Environ.push_named (rel_name,None, 
-						 fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities
+						 fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
@@ -1395,7 +1397,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    ((Loc.ghost,relnames.(i)),
+    (((Loc.ghost,relnames.(i)), None),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
@@ -1460,8 +1462,17 @@ let do_build_inductive
 
 
 let build_inductive evd funconstants funsargs returned_types rtl =
+  let pu = !Detyping.print_universes in
+  let cu = !Constrextern.print_universes in
   try
-    do_build_inductive evd funconstants funsargs returned_types rtl
-  with e when Errors.noncritical e -> raise (Building_graph e)
+    Detyping.print_universes := true;
+    Constrextern.print_universes := true;
+    do_build_inductive evd funconstants funsargs returned_types rtl;
+    Detyping.print_universes := pu;
+    Constrextern.print_universes := cu
+  with e when Errors.noncritical e ->
+    Detyping.print_universes := pu;
+    Constrextern.print_universes := cu;
+    raise (Building_graph e)
 
 
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 0f10636f..179e8fe8 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -6,7 +6,7 @@ open Misctypes
 val get_pattern_id : cases_pattern -> Id.t list
 
 (* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
-   [pat] must not contain occurences of anonymous pattern
+   [pat] must not contain occurrences of anonymous pattern
 *)
 val pattern_to_term : cases_pattern -> glob_constr
 
@@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
 
 (* [alpha_pat avoid pat] rename all the variables present in [pat] s.t.
    the result does not share variables with [avoid]. This function create
-   a fresh variable for each occurence of the anonymous pattern.
+   a fresh variable for each occurrence of the anonymous pattern.
 
    Also returns a mapping  from old variables to new ones and the concatenation of
    [avoid] with the variables appearing in the result.
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e211b688..3dbd4380 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -27,7 +27,6 @@ let choose_dest_or_ind scheme_info =
   Tactics.induction_destruct (is_rec_info scheme_info) false
 
 let functional_induction with_clean c princl pat =
-  Dumpglob.pause ();
   let res =
     let f,args = decompose_app c in
     fun g ->
@@ -72,11 +71,11 @@ let functional_induction with_clean c princl pat =
 		    errorlabstrm "" (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
-	      (princ,NoBindings, Tacmach.pf_type_of g' princ,g')
+	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
 	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
-	 princ,binding,Tacmach.pf_type_of g princ,g
+	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
     in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     let args_as_induction_constr =
@@ -123,9 +122,7 @@ let functional_induction with_clean c princl pat =
 	 (args_as_induction_constr,princ')))
       subst_and_reduce
       g'
-  in
-    Dumpglob.continue ();
-    res
+  in res
 
 let rec abstract_glob_constr c = function
   | [] -> c
@@ -145,15 +142,14 @@ let interp_casted_constr_with_implicits env sigma impls c  =
 
 let build_newrecursive
     lnameargsardef  =
-  let env0 = Global.env()
-  and sigma = Evd.empty
-  in
+  let env0 = Global.env() in
+  let sigma = Evd.from_env env0 in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) ((_,recname),bl,arityc,_) ->
+      (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
-	let evdref =  ref (Evd.from_env env0) in
+	let evdref = ref (Evd.from_env env0) in
 	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
         (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
@@ -228,7 +224,7 @@ let process_vernac_interp_error e =
 
 let derive_inversion fix_names =
   try
-    let evd' = Evd.empty in 
+    let evd' = Evd.from_env (Global.env ()) in 
     (* we first transform the fix_names identifier into their corresponding constant *)
     let evd',fix_names_as_constant =
       List.fold_right
@@ -323,7 +319,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
       Tacmach.tactic) : unit =
-  let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in
+  let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -343,7 +339,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 		 locate_ind
 		 f_R_mut)
 	in
-	let fname_kn ((fname,_,_,_,_),_) =
+	let fname_kn (((fname,_),_,_,_,_),_) =
 	  let f_ref = Ident fname in
 	  locate_with_msg
 	    (pr_reference f_ref++str ": Not an inductive type!")
@@ -355,9 +351,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	  List.map_i
 	    (fun i x ->
 	     let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
-	     let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in
-	     let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in
-	     let _ = evd := evd' in 
+	     let env = Global.env () in
+	     let evd = ref (Evd.from_env env) in
+	     let evd',uprinc = Evd.fresh_global env !evd princ in
+             let _ = evd := evd' in 
+	     let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
@@ -380,21 +378,21 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
-    | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+    | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
       Command.do_definition
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition)
+	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
 	    evd,((destConst c)::l)
 	   )
-	   (Evd.empty,[])
+	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
        evd,List.rev rev_pconstants
@@ -402,13 +400,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
 	    evd,((destConst c)::l)
 	   )
-	   (Evd.empty,[])
+	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
        evd,List.rev rev_pconstants
@@ -594,9 +592,9 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
+  let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
-    with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in
+    with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
      
@@ -614,7 +612,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   let _is_struct =
     match fixpoint_exprl with
       | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- 	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
+ 	  let (((((_,name),pl),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -625,7 +623,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  let using_lemmas = [] in 
 	  let pre_hook pconstants =
 	    generate_principle
-	      (ref (Evd.empty))
+	      (ref (Evd.from_env (Global.env ())))
 	      pconstants
 	      on_error
 	      true
@@ -638,7 +636,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
 	  false
       |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- 	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
+ 	  let (((((_,name),_),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -649,7 +647,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	  let pre_hook pconstants =
 	    generate_principle
-	      (ref Evd.empty)
+	      (ref (Evd.from_env (Global.env ())))
 	      pconstants
 	      on_error
 	      true
@@ -672,7 +670,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	    fixpoint_exprl;
 	let fixpoint_exprl = recompute_binder_list fixpoint_exprl in 
 	let fix_names =
-	  List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl
+	  List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
 	in
 	(* ok all the expressions are structural *)
   	let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -680,7 +678,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	let evd,pconstants =
 	  if register_built
 	  then register_struct is_rec fixpoint_exprl
-	  else (Evd.empty,pconstants)
+	  else (Evd.from_env (Global.env ()),pconstants)
 	in
 	let evd = ref evd in 
 	generate_principle
@@ -830,15 +828,15 @@ let make_graph (f_ref:global_reference) =
 	  end
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
-  Dumpglob.pause ();
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom !"
      | Some body ->
 	 let env = Global.env () in
+	 let sigma = Evd.from_env env in
 	 let extern_body,extern_type =
 	   with_full_print (fun () ->
-		(Constrextern.extern_constr false env Evd.empty body,
-		 Constrextern.extern_type false env Evd.empty
+		(Constrextern.extern_constr false env sigma body,
+		 Constrextern.extern_type false env sigma
                    ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
 		)
 	     )
@@ -867,22 +865,21 @@ let make_graph (f_ref:global_reference) =
 			    )
 			in
 			let b' = add_args (snd id) new_args b in
-			(((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+			((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
 		let id = Label.to_id (con_label c) in
-		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+		 [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 let mp,dp,_ = repr_con c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
-	   expr_list);
-  Dumpglob.continue ()
+	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 738ade8c..aa47e261 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,9 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Constrintern.locate_reference princ_ref
-  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
+  with Not_found ->
+    Errors.errorlabstrm "IndFun.const_of_id"
+      (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
@@ -147,7 +149,7 @@ let get_locality = function
 | Global -> false
 
 let save with_clean id const (locality,_,kind) hook =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+  let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
@@ -178,9 +180,10 @@ let get_proof_clean do_reduce =
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
-  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () 
-  in
+  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
+  let old_printuniverses = !Constrextern.print_universes in
+  Constrextern.print_universes := true;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
@@ -193,6 +196,7 @@ let with_full_print f a =
     Impargs.make_strict_implicit_args old_strict_implicit_args;
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
+    Constrextern.print_universes := old_printuniverses;
     Dumpglob.continue ();
     res
   with
@@ -201,6 +205,7 @@ let with_full_print f a =
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
+	Constrextern.print_universes := old_printuniverses;
 	Dumpglob.continue ();
 	raise reraise
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 10daf6e8..23f1da1b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Lemmas.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
@@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
 *)
 val get_proof_clean : bool ->
   Names.Id.t *
-    (Entries.definition_entry * Decl_kinds.goal_kind)
+    (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
 
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d10924f8..d9794014 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i =
   let evd',graph =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
   in
-  let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in
   evd:=evd';
+  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -193,7 +193,7 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
 
@@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_type_of g (mkVar hid) in
+	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
 	     match kind_of_term type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
@@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true)  gl term in
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_type_of g (mkVar id)) with
+	       match kind_of_term  (pf_unsafe_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta schemes.(i)  in
-    let princ_type = pf_type_of g graph_principle in
+    let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
@@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   let funs_constr = Array.map mkConstU funs  in
   States.with_state_protection_on_exception
     (fun () ->
-     let evd = ref Evd.empty in 
+     let env = Global.env () in
+     let evd = ref (Evd.from_env env) in 
      let graphs_constr = Array.map mkInd graphs in
      let lemmas_types_infos =
        Util.Array.map2_i
@@ -772,7 +773,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in 
+	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
@@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 
       )
       funs;
-    (* let evd = ref Evd.empty in  *)
     let lemmas_types_infos =
       Util.Array.map2_i
 	(fun i f_constr graph ->
@@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))  !evd
+	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
@@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_type_of g (mkVar hid) in
+    let typ = pf_unsafe_type_of g (mkVar hid) in
     match kind_of_term typ with
       | App(i,args) when isInd i ->
 	  let ((kn',num) as ind'),u = destInd i in
@@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_type_of g (mkVar hid) in
+    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1003,7 +1003,7 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_type_of g (mkVar hid)  in
+	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (make_eq ()) ->
 		   begin
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580..e3455e77 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     (rawlist:(Id.t * glob_constr) list) =
-  let lident = Loc.ghost, shift.ident in
+  let lident = (Loc.ghost, shift.ident), None in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
   let lcstor_expr : (bool * (lident * constr_expr)) list  =
@@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,impls = Command.interp_mutual_inductive indl [] 
+  let mie,pl,impls = Command.interp_mutual_inductive indl []
           false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (Command.declare_mutual_inductive_with_eliminations mie impls)
+  ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
 
 
 (* Find infos on identifier id. *)
@@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
-    [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
+    [ind1] and [ind2]. identifiers occurring in both arrays [args1] and
     [args2] are considered linked (i.e. are the same variable) in the
     new graph.
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0999b95d..5d41ec72 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,7 +115,7 @@ let pf_get_new_ids idl g =
 
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_type_of gls c)
+    (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) =
 			       Anonymous)],
 	  GVar(d0,v_id)])
     in
-    let body = fst (understand env Evd.empty glob_body)(*FIXME*) in
+    let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
 let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -305,7 +305,8 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then error ("check_not_nested : failure "^Id.to_string x)
+        then errorlabstrm "Recdef.check_not_nested"
+               (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -399,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    thin to_intros;
 	    h_intros to_intros;
 	    (fun g' -> 
-	      let ty_teq = pf_type_of g' (mkVar heq) in
+	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
 		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
@@ -513,13 +514,13 @@ let rec prove_lt hyple g =
       in
       let h =
 	List.find (fun id ->
-          match decompose_app (pf_type_of g (mkVar id)) with
+          match decompose_app (pf_unsafe_type_of g (mkVar id)) with
             | _, t::_ -> eq_constr t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
+	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
       observe_tclTHENLIST (str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
@@ -654,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
 let pf_type c tac gl = 
-  let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
 let pf_typel l tac =
@@ -679,7 +680,7 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_type_of g expr in
+  let type_of_expr = pf_unsafe_type_of g expr in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
@@ -1292,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
+    let env = Global.env () in
     Proof_global.discard_all ();
-    build_proof Evd.empty
+    build_proof (Evd.from_env env)
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   observe_tclTHENLIST (str "")
@@ -1397,9 +1399,7 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    let sigma =
-      Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env
-    in
+    let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
     open_new_goal start_proof sigma
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
@@ -1436,9 +1436,7 @@ let (com_eqn : int -> Id.t ->
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
     in
     let (evmap, env) = Lemmas.get_current_context() in
-    let evmap =
-      Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env
-    in
+    let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
@@ -1511,12 +1509,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     fst (*FIXME*)(interp_constr
       env_with_pre_rec_args
-      Evd.empty
+      (Evd.from_env env_with_pre_rec_args)
       r)
   in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 88c1a783..a36369d2 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -23,7 +23,7 @@ struct
 	  - None , Some v -> \]-oo,v\]
 	  - Some v, None  -> \[v,+oo\[
 	  - Some v, Some v' -> \[v,v'\]
-      Intervals needs to be explicitely normalised.
+      Intervals needs to be explicitly normalised.
       *)
 
   type who = Left | Right
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 37428c39..aac9a7d3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -539,7 +539,7 @@ let context operation path (t : constr) =
   in
   loop 1 path t
 
-let occurence path (t : constr) =
+let occurrence path (t : constr) =
   let rec loop p0 t = match (p0,kind_of_term t) with
     | (p, Cast (c,_,_)) -> loop p c
     | ([], _) -> t
@@ -555,7 +555,7 @@ let occurence path (t : constr) =
     | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
     | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
     | (p, _) ->
-	failwith ("occurence " ^ string_of_int(List.length p))
+	failwith ("occurrence " ^ string_of_int(List.length p))
   in
   loop path t
 
@@ -660,7 +660,7 @@ let clever_rewrite_gen_nat p result (t,args) =
 let clever_rewrite p vpath t gl =
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
-  let vargs = List.map (fun p -> occurence p occ) vpath in
+  let vargs = List.map (fun p -> occurrence p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   exact (applist(t',[mkNewMeta()])) gl
 
@@ -1462,7 +1462,7 @@ let coq_omega =
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
       Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
+    with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
   end
   end
 
@@ -1689,7 +1689,7 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of = Tacmach.New.pf_type_of gl in
+  let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = Tacmach.New.of_old decidability gl in
   let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 8156e841..95407c5f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -44,7 +44,7 @@ let occ_step_eq s1 s2 = match s1, s2 with
 
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
+type occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
 
 (* \subsection{refiable formulas} *)
 type oformula =
@@ -81,7 +81,7 @@ and oequation = {
     e_left: oformula;			(* formule brute gauche *)
     e_right: oformula;			(* formule brute droite *)
     e_trace: Term.constr;		(* tactique de normalisation *)
-    e_origin: occurence;		(* l'hypothèse dont vient le terme *)
+    e_origin: occurrence;		(* l'hypothèse dont vient le terme *)
     e_negated: bool;			(* vrai si apparait en position nié
 					   après normalisation *)
     e_depends: direction  list;		(* liste des points de disjonction dont
@@ -111,7 +111,7 @@ type environment = {
   real_indices : (int,int) Hashtbl.t;
   mutable cnt_connectors : int;
   equations : (int,oequation) Hashtbl.t;
-  constructors : (int, occurence) Hashtbl.t
+  constructors : (int, occurrence) Hashtbl.t
 }
 
 (* \subsection{Solution tree}
@@ -136,7 +136,7 @@ type solution_tree =
    chemins pour extraire des equations ou d'hypothèses *)
 
 type context_content =
-    CCHyp of occurence
+    CCHyp of occurrence
   | CCEqua of int
 
 (* \section{Specific utility functions to handle base types} *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509..c7185ff2 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -155,14 +155,19 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 (****************************************************************************)
 
 let ic c =
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   Constrintern.interp_open_constr env sigma c
 
 let ic_unsafe c = (*FIXME remove *)
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
     fst (Constrintern.interp_constr env sigma c)
 
-let ty c = Typing.type_of (Global.env()) Evd.empty c
+let ty c =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+    Typing.unsafe_type_of env sigma c
 
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
@@ -215,7 +220,7 @@ let exec_tactic env evd n f args =
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
-    Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd
+    Array.map (fun x -> nf (constr_of x)) !res, snd (Evd.universe_context evd)
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];