Merge PR#696: Trunk+cleanup constr of global

29 files changed, 271 insertions, 218 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 3f3b0a870..bcda4ff50 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -119,13 +119,17 @@ In Coqlib / reference location:
   We have removed from Coqlib functions returning `constr` from
   names. Now it is only possible to obtain references, that must be
   processed wrt the particular needs of the client.
+  We have changed in constrintern the functions returnin `constr` as
+  well to return global references instead.
 
   Users of `coq_constant/gen_constant` can do
   `Universes.constr_of_global (find_reference dir r)` _however_ note
   the warnings in the `Universes.constr_of_global` in the
   documentation. It is very likely that you were previously suffering
   from problems with polymorphic universes due to using
-  `Coqlib.coq_constant` that used to do this.
+  `Coqlib.coq_constant` that used to do this. You must rather use
+  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
+  when constructing terms in ML (see univpoly.txt for more information).
 
 ** Tactic API **
 
@@ -133,6 +137,10 @@ In Coqlib / reference location:
   Thus it only generates one instance of the global reference, and it is the
   caller's responsibility to perform a focus on the goal.
 
+- pf_global, construct_reference, global_reference,
+  global_reference_in_absolute_module now return a global_reference
+  instead of a constr.
+
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c0485e4e7..5a05150d4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -782,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
     Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
   Sigma.Sigma (of_constr t,sigma,p)
 
+let is_global sigma gr c =
+  Globnames.is_global gr (to_constr sigma c)
+
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9d705b4d5..9f45187cf 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -261,6 +261,8 @@ val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
   'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
 
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
 (** {5 Extra} *)
 
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 81ebf6561..190369e8f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -98,16 +98,16 @@ let global_reference_of_reference ref =
   locate_reference (snd (qualid_of_reference ref))
 
 let global_reference id =
-  Universes.constr_of_global (locate_reference (qualid_of_ident id))
+  locate_reference (qualid_of_ident id)
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Context.Named.lookup id ctx in id)
+    VarRef (let _ = Context.Named.lookup id ctx in id)
   with Not_found ->
     global_reference id
 
 let global_reference_in_absolute_module dir id =
-  Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+  Nametab.global_of_path (Libnames.make_path dir id)
 
 (**********************************************************************)
 (* Internalization errors                                             *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644cafe57..644f60d85 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -176,9 +176,9 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
-val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
+val global_reference : Id.t -> Globnames.global_reference
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b3017f359..43c06a54d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms =
 let build_projection intype (cstr:pconstructor) special default gls=
   let open Tacmach.New in
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
-    mkLambda(Name id,intype,body)
+  sigma, mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
@@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
-         let proj =
+         let sigma, proj =
            build_projection intype cstr special default gl
          in
 	 let injt=
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
-	   Tacticals.New.tclTHEN injt (proof_tac prf)))
+	 Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+                               (Tacticals.New.tclTHEN injt (proof_tac prf))))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b2c8489ce..763443717 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -133,20 +133,6 @@ let prNamedRLDecl s lc =
     prstr "\n";
   end
 
-let showind (id:Id.t) =
-  let cstrid = Constrintern.global_reference id in
-  let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
-  let u = EConstr.Unsafe.to_instance u in
-  List.iter (fun decl ->
-    print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
-    prconstr (RelDecl.get_type decl); print_string "\n")
-    ib1.mind_arity_ctxt;
-    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
-  Array.iteri
-    (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
-    ib1.mind_user_lc
-
 (** {2 Misc} *)
 
 exception Found of int
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cba9c1364..9726a5b40 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,8 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let p = EConstr.of_constr @@ Universes.constr_of_global p in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let p = EConstr.of_constr p in
   let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
@@ -735,7 +736,6 @@ let rewrite_except h =
 
 let refl_equal = 
   let coq_base_constant s =
-    Universes.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition"
       (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in
   function () -> (coq_base_constant "eq_refl")
@@ -747,8 +747,9 @@ let refl_equal =
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
-       Tacticals.New.tclTHENLIST
-         [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
+    Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
+    Tacticals.New.tclTHENLIST
+         [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
           Proofview.Goal.enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 966b11d0e..dadcfb9f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -751,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let make_eq_refl () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
+let new_global (evars, cstrs) gr = 
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr
+  in (Sigma.to_evar_map sigma, cstrs), c
 
-let get_rew_prf r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel, prf 
+let make_eq sigma =
+  new_global sigma (Coqlib.build_coq_eq ())
+let make_eq_refl sigma =
+  new_global sigma (Coqlib.build_coq_eq_refl ())
+
+let get_rew_prf evars r = match r.rew_prf with
+  | RewPrf (rel, prf) -> evars, (rel, prf)
   | RewCast c ->
-    let rel = mkApp (make_eq (), [| r.rew_car |]) in
-      rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]),
-		   c, mkApp (rel, [| r.rew_from; r.rew_to |]))
+    let evars, eq = make_eq evars in
+    let evars, eq_refl = make_eq_refl evars in
+    let rel = mkApp (eq, [| r.rew_car |]) in
+    evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
+		         c, mkApp (rel, [| r.rew_from; r.rew_to |])))
 
 let poly_subrelation sort = 
   if sort then PropGlobal.subrelation else TypeGlobal.subrelation
@@ -827,7 +833,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 		      env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
 	      | Some r ->
-		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, 
+                 let evars, proof = get_rew_prf evars r in
+		 [ snd proof; r.rew_to; x ] @ acc, subst, evars, 
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
@@ -847,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res =
   | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
 
 let coerce env avoid cstr res = 
-  let rel, prf = get_rew_prf res in
+  let evars, (rel, prf) = get_rew_prf res.rew_evars res in
+  let res = { res with rew_evars = evars } in
     apply_constraint env avoid res.rew_car rel prf cstr res
 
 let apply_rule unify loccs : int pure_strategy =
@@ -868,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy =
 	    else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
 	    else
 	      let res = { rew with rew_car = ty } in
-              let rel, prf = get_rew_prf res in
-	      let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
+	      let res = Success (coerce env unfresh cstr res) in
               (occ, res)
     }
 
@@ -1231,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 	in 
 	let res = 
 	  match res with
-	  | Success r ->  
-	    let rel, prf = get_rew_prf r in
-	      Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
+	  | Success r -> Success (coerce env unfresh (prop,cstr) r)
 	  | Fail | Identity -> res
 	in state, res
       | _ -> state, Fail
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index f5e6f05ce..2858df313 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Stdarg
 open Tacarg
 open Misctypes
 open Globnames
-open Term
 open Genredexpr
 open Patternops
 
@@ -91,7 +90,7 @@ open Printer
 let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
-   if not (eq_constr (Universes.constr_of_global ref') t') then
+   if not (is_global ref' t') then
     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4ec111e01..d8e21d81d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -220,9 +220,7 @@ let apply_nnpp _ ist =
   Proofview.tclBIND
     (Proofview.tclUNIT ())
     begin fun () -> try
-      let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
-      let nnpp = EConstr.of_constr nnpp in
-      apply nnpp
+      Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply
     with Not_found -> tclFAIL 0 (Pp.mt ())
     end
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ee748567b..d7408e88e 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -39,10 +39,10 @@ open OmegaSolver
 
 let elim_id id =
   Proofview.Goal.enter { enter = begin fun gl ->
-    simplest_elim (Tacmach.New.pf_global id gl)
+    simplest_elim (mkVar id)
   end }
 let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
-  apply (Tacmach.New.pf_global id gl)
+  apply (mkVar id)
 end }
 
 let timing timer_name f arg = f arg
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 7412de1e8..ba8356b52 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -456,39 +456,56 @@ let quote_terms env sigma ivs lc =
   term. Ring for example needs that, but Ring doesn't use Quote
   yet. *)
 
+let pf_constrs_of_globals l =
+  let rec aux l acc =
+    match l with
+      [] -> Proofview.tclUNIT (List.rev acc)
+    | hd :: tl ->
+       Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc)
+  in aux l []
+
 let quote f lid =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = Tacmach.New.project gl in
-    let f = Tacmach.New.pf_global f gl in
-    let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
-    let ivs = compute_ivs f cl gl in
-    let concl = Proofview.Goal.concl gl in
-    let quoted_terms = quote_terms env sigma ivs [concl] in
-    let (p, vm) = match quoted_terms with
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let fg = Tacmach.New.pf_global f gl in
+    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+    Tacticals.New.pf_constr_of_global fg >>= fun f ->
+    pf_constrs_of_globals clg >>= fun cl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Tacmach.New.project gl in
+      let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in
+      let concl = Proofview.Goal.concl gl in
+      let quoted_terms = quote_terms env sigma ivs [concl] in
+      let (p, vm) = match quoted_terms with
       | [p], vm -> (p,vm)
       | _ -> assert false
-    in
-    match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
-    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+      in
+      match ivs.variable_lhs with
+      | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+      | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+    end }
   end }
 
 let gen_quote cont c f lid =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let env = Proofview.Goal.env gl in
-  let sigma = Tacmach.New.project gl in
-  let f = Tacmach.New.pf_global f gl in
-  let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
-  let ivs = compute_ivs f cl gl in
-  let quoted_terms = quote_terms env sigma ivs [c] in
-  let (p, vm) = match quoted_terms with
-    | [p], vm -> (p,vm)
-    | _ -> assert false
-  in
-  match ivs.variable_lhs with
-    | None -> cont (mkApp (f, [| p |]))
-    | Some _ -> cont (mkApp (f, [| vm; p |]))
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let fg = Tacmach.New.pf_global f gl in
+    let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+    Tacticals.New.pf_constr_of_global fg >>= fun f ->
+    pf_constrs_of_globals clg >>= fun cl ->
+    Proofview.Goal.nf_enter { enter = begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Tacmach.New.project gl in
+      let cl = List.map (EConstr.to_constr sigma) cl in
+      let ivs = compute_ivs f cl gl in
+      let quoted_terms = quote_terms env sigma ivs [c] in
+      let (p, vm) = match quoted_terms with
+        | [p], vm -> (p,vm)
+        | _ -> assert false
+      in
+      match ivs.variable_lhs with
+      | None -> cont (mkApp (f, [| p |]))
+      | Some _ -> cont (mkApp (f, [| vm; p |]))
+    end }
   end }
 
 (*i
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 38c75fcf8..80680e408 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign =
 	   (Some ([], 0, 0, [])) eqnpats pats
 	 in match acc with
 	     None -> c
-	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
-		 (lift_rel_context liftsign sign)
-	       in
-		 conj :: c)
+	    | Some (sign, len, _, c') ->
+               let sigma, conj = mk_coq_and !evdref c' in
+               let sigma, neg = mk_coq_not sigma conj in
+	       let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in
+               evdref := sigma; conj :: c)
       [] prevpatterns
   in match diffs with [] -> None
-    | _ -> Some (mk_coq_and diffs)
+    | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj)
 
 let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
   let i = ref 0 in
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8769c5659..2fa3facb3 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 
-let init_constant  dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s
 let init_reference dir s () = Coqlib.coq_reference  "Program" dir s
 
 let papp evdref r args = 
@@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect"
 let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq"
 let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
 
-let coq_not = init_constant ["Init";"Logic"] "not"
-let coq_and = init_constant ["Init";"Logic"] "and"
+let coq_not = init_reference ["Init";"Logic"] "not"
+let coq_and = init_reference ["Init";"Logic"] "and"
 
-let delayed_force c = EConstr.of_constr (c ())
+let new_global sigma gr =
+  let open Sigma in
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
 
-let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |])
+let mk_coq_not sigma x =
+  let sigma, notc = new_global sigma (coq_not ()) in
+  sigma, EConstr.mkApp (notc, [| x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
   | [] -> invalid_arg "unsafe_fold_right"
 
-let mk_coq_and l =
-  let and_typ = delayed_force coq_and in
-    unsafe_fold_right
+let mk_coq_and sigma l =
+  let sigma, and_typ = new_global sigma (coq_and ()) in
+  sigma, unsafe_fold_right
       (fun c conj ->
 	 EConstr.mkApp (and_typ, [| c ; conj |]))
       l
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 94a7bdcb6..8439b9528 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference
 val coq_JMeq_ind : unit -> global_reference
 val coq_JMeq_refl : unit -> global_reference
 
-val mk_coq_and : constr list -> constr
-val mk_coq_not : constr -> constr
+val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
+val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
 
 (** Polymorphic application of delayed references *)
 val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 97c5cda77..66d91c634 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
+let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -171,7 +171,7 @@ module New = struct
     (** We only check for the existence of an [id] in [hyps] *)
     let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
-    EConstr.of_constr (Constrintern.construct_reference hyps id)
+    Constrintern.construct_reference hyps id
 
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e6e60e27f..1172e55ac 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -100,7 +100,7 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
-  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index fe44559ed..5e7090ded 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -19,10 +19,9 @@ module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
-let mk_absurd_proof t =
-  let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
+let mk_absurd_proof coq_not t =
   let id = Namegen.default_dependent_ident in
-  mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
+  mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
@@ -34,9 +33,11 @@ let absurd c =
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
     let tac =
+    Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
+    Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
-      elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
-      Simple.apply (mk_absurd_proof t)
+      elim_type coqfalse;
+      Simple.apply (mk_absurd_proof coqnot t)
     ] in
     Sigma.Unsafe.of_pair (tac, sigma)
   end }
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bda25d7f0..48ce52f09 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,14 +104,9 @@ let solveNoteqBranch side =
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let make_eq () =
-(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ())
-let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ())
-
-let mkDecideEqGoal eqonleft op rectype c1 c2 =
-  let equality    = mkApp(make_eq(), [|rectype; c1; c2|]) in
-  let disequality = mkApp(build_coq_not (), [|equality|]) in
+let mkDecideEqGoal eqonleft (op,eq,neg) rectype c1 c2 =
+  let equality    = mkApp(eq, [|rectype; c1; c2|]) in
+  let disequality = mkApp(neg, [|equality|]) in
   if eqonleft then mkApp(op, [|equality; disequality |])
   else mkApp(op, [|disequality; equality |])
 
@@ -121,13 +116,13 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 =
 let idx = Id.of_string "x"
 let idy = Id.of_string "y"
 
-let mkGenDecideEqGoal rectype g =
+let mkGenDecideEqGoal rectype ops g =
   let hypnames = pf_ids_of_hyps g in
   let xname    = next_ident_away idx hypnames
   and yname    = next_ident_away idy hypnames in
   (mkNamedProd xname rectype
      (mkNamedProd yname rectype
-        (mkDecideEqGoal true (build_coq_sumbool ())
+        (mkDecideEqGoal true ops
           rectype (mkVar xname) (mkVar yname))))
 
 let rec rewrite_and_clear hyps = match hyps with
@@ -256,9 +251,9 @@ let decideGralEquality =
 
 let decideEqualityGoal = tclTHEN intros decideGralEquality
 
-let decideEquality rectype =
+let decideEquality rectype ops =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let decide = mkGenDecideEqGoal rectype gl in
+  let decide = mkGenDecideEqGoal rectype ops gl in
   (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
   end }
 
@@ -266,11 +261,15 @@ let decideEquality rectype =
 (* The tactic Compare *)
 
 let compare c1 c2 =
+  pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
+  pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
+  pf_constr_of_global (build_coq_not ()) >>= fun notc ->
   Proofview.Goal.enter { enter = begin fun gl ->
   let rectype = pf_unsafe_type_of gl c1 in
-  let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
+  let ops = (opc,eqc,notc) in
+  let decide = mkDecideEqGoal true ops rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro
              (tclTHEN (onLastHyp simplest_case) clear_last));
-             decideEquality rectype])
+             decideEquality rectype ops])
   end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e6278943d..268daf6b6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -874,7 +874,7 @@ let descend_then env sigma head dirn =
   let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in
   (dirn_nlams,
    dirn_env,
-   (fun dirnval (dfltval,resty) ->
+   (fun sigma dirnval (dfltval,resty) ->
       let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
@@ -887,7 +887,7 @@ let descend_then env sigma head dirn =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
+      sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -932,23 +932,28 @@ let build_selector env sigma dirn c ind special default =
   let brl =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
-  mkCase (ci, p, c, Array.of_list brl)
+  sigma, mkCase (ci, p, c, Array.of_list brl)
 
-let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())
-let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ())
-let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ())
+let new_global sigma gr =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
+    
+let build_coq_False sigma = new_global sigma (build_coq_False ())
+let build_coq_True sigma = new_global sigma (build_coq_True ())
+let build_coq_I sigma = new_global sigma (build_coq_I ())
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
-      let true_0,false_0 =
-        build_coq_True(),build_coq_False() in
+      let sigma, true_0 = build_coq_True sigma in
+      let sigma, false_0 = build_coq_False sigma in
       build_selector env sigma dirn c ind true_0 false_0
   | ((sp,cnum),argnum)::l ->
+      let sigma, false_0 = build_coq_False sigma in
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
-      let subval = build_discriminator cnum_env sigma dirn newc l in
-      kont subval (build_coq_False (),mkSort (Prop Null))
+      let sigma, subval = build_discriminator cnum_env sigma dirn newc l in
+      kont sigma subval (false_0,mkSort (Prop Null))
 
 (* Note: discrimination could be more clever: if some elimination is
    not allowed because of a large impredicative constructor in the
@@ -991,9 +996,9 @@ let ind_scheme_of_eq lbeq =
 
 
 let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
-  let i            = build_coq_I () in
-  let absurd_term  = build_coq_False () in
-  let eq_elim, eff = ind_scheme_of_eq lbeq in
+  let sigma, i           = build_coq_I sigma in
+  let sigma, absurd_term = build_coq_False sigma in
+  let eq_elim, eff       = ind_scheme_of_eq lbeq in
   let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
   let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
@@ -1013,7 +1018,7 @@ let apply_on_clause (f,t) clause =
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
-  let discriminator =
+  let sigma, discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
@@ -1309,7 +1314,8 @@ let rec build_injrec env sigma dflt c = function
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
       let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in
-	sigma, (kont subval (dfltval,tuplety), tuplety,dfltval)
+      let sigma, res = kont sigma subval (dfltval,tuplety) in
+      sigma, (res, tuplety,dfltval)
     with
 	UserError _ -> failwith "caught"
 
@@ -1326,8 +1332,6 @@ let inject_if_homogenous_dependent_pair ty =
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
-    let ceq = Universes.constr_of_global Coqlib.glob_eq in
-    let ceq = EConstr.of_constr ceq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
     let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
@@ -1346,16 +1350,18 @@ let inject_if_homogenous_dependent_pair ty =
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
-    let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@
-      Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"]
+                                    "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
+        Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq ->
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
+           Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
            Proofview.V82.tactic (Tacmach.refine
              (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
diff --git a/tactics/equality.mli b/tactics/equality.mli
index b47be3bbc..27be5affb 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
 (* [build_selector env sigma i c t u v] matches on [c] of
    type [t] and returns [u] in branch [i] and [v] on other branches *)
 val build_selector : env -> evar_map -> int -> constr -> types ->
-  constr -> constr -> constr
+  constr -> constr -> evar_map * constr
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 35fbec5a6..2ba18ceb4 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -544,7 +544,7 @@ let match_eqdec sigma t =
         false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
-      eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ
+      eqonleft, Lazy.force op, c1, c2, typ
   | _ -> anomaly (Pp.str "Unexpected pattern")
 
 (* Patterns "~ ?" and "? -> False" *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 82a3d47b5..9110830aa 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -142,7 +142,7 @@ val is_matching_sigma : evar_map -> constr -> bool
 
 (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
    [t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr
+val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b443a357a..6e45739ec 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3519,27 +3519,32 @@ let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
   user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
-let glob c = EConstr.of_constr (Universes.constr_of_global c)
+let glob sigma gr =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
 
-let coq_eq      = lazy (glob (Coqlib.build_coq_eq ()))
-let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ()))
+let coq_eq sigma       = glob sigma (Coqlib.build_coq_eq ())
+let coq_eq_refl sigma  = glob sigma (Coqlib.build_coq_eq_refl ())
 
-let coq_heq      = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq"))
-let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl"))
+let coq_heq_ref        = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq sigma      = glob sigma (Lazy.force coq_heq_ref)
+let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
-let mkEq t x y =
-  mkApp (Lazy.force coq_eq, [| t; x; y |])
+let mkEq sigma t x y =
+  let sigma, eq = coq_eq sigma in
+  sigma, mkApp (eq, [| t; x; y |])
 
-let mkRefl t x =
-  mkApp (Lazy.force coq_eq_refl, [| t; x |])
+let mkRefl sigma t x =
+  let sigma, refl = coq_eq_refl sigma in
+  sigma, mkApp (refl, [| t; x |])
 
-let mkHEq t x u y =
-  mkApp (Lazy.force coq_heq,
-	[| t; x; u; y |])
+let mkHEq sigma t x u y =
+  let sigma, c = coq_heq sigma in
+  sigma, mkApp (c,[| t; x; u; y |])
 
-let mkHRefl t x =
-  mkApp (Lazy.force coq_heq_refl,
-	[| t; x |])
+let mkHRefl sigma t x =
+  let sigma, c = coq_heq_refl sigma in
+  sigma, mkApp (c, [| t; x |])
 
 let lift_togethern n l =
   let l', _ =
@@ -3577,23 +3582,30 @@ let decompose_indapp sigma f args =
 	mkApp (f, pars), args
   | _ -> f, args
 
-let mk_term_eq env sigma ty t ty' t' =
+let mk_term_eq homogeneous env sigma ty t ty' t' =
   let sigma = Sigma.to_evar_map sigma in
-  if Reductionops.is_conv env sigma ty ty' then
-    mkEq ty t t', mkRefl ty' t'
+  if homogeneous then
+    let sigma, eq = mkEq sigma ty t t' in
+    let sigma, refl = mkRefl sigma ty' t' in
+    Sigma.Unsafe.of_evar_map sigma, (eq, refl)
   else
-    mkHEq ty t ty' t', mkHRefl ty' t'
+    let sigma, heq = mkHEq sigma ty t ty' t' in
+    let sigma, hrefl = mkHRefl sigma ty' t' in
+    Sigma.Unsafe.of_evar_map sigma, (heq, hrefl)
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let open Context.Rel.Declaration in
   Refine.refine { run = begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
-  let abshypeq, abshypt =
+  let sigma, abshypeq, abshypt =
     if dep then
-      let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in
-	mkProd (Anonymous, eq, lift 1 concl), [| refl |]
-    else concl, [||]
+      let ty = lift 1 c in
+      let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in
+      let sigma, (eq, refl) =
+        mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in
+      sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |]
+    else sigma, concl, [||]
   in
     (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
@@ -3699,9 +3711,13 @@ let abstract_args gl generalize_vars dep id defined f args =
 	  let liftarg = lift (List.length ctx) arg in
 	  let eq, refl =
 	    if leq then
-	      mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg
+	      let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in
+              let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in
+              sigma := sigma'; eq, refl
 	    else
-	      mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
+	      let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in
+              let sigma', refl = mkHRefl sigma' argty arg in
+              sigma := sigma'; eq, refl
 	  in
 	  let eqs = eq :: lift_list eqs in
 	  let refls = refl :: refls in
@@ -3801,17 +3817,19 @@ let specialize_eqs id gl =
     match EConstr.kind !evars ty with
     | Prod (na, t, b) ->
 	(match EConstr.kind !evars t with
-	| App (eq, [| eqty; x; y |]) when EConstr.eq_constr !evars (Lazy.force coq_eq) eq ->
+	| App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq ->
 	    let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
-	    let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
-	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
+	    let pt = mkApp (eq, [| eqty; c; c |]) in
+            let ind = destInd !evars eq in
+	    let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty
-	| App (heq, [| eqty; x; eqty'; y |]) when EConstr.eq_constr !evars heq (Lazy.force coq_heq) ->
+	| App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
 	    let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
-	    let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
-	    let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
+	    let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
+            let ind = destInd !evars heq in
+	    let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty
diff --git a/vernac/command.ml b/vernac/command.ml
index 29cde4d3d..87e7e50ec 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -211,7 +211,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
-	| None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c))
+	| None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
       in 
       Obligations.check_evars env evd;
       let obls, _, c, cty = 
@@ -907,23 +907,26 @@ let fixsub_module = subtac_dir @ ["Wf"]
 let tactics_module = subtac_dir @ ["Tactics"]
 
 let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant  dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s)
+let init_constant  dir s evdref =
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref)
+                                                (Coqlib.coq_reference "Command" dir s)
+  in evdref := Sigma.to_evar_map sigma; c
 
 let make_ref l s = init_reference l s
 let fix_proto = init_constant tactics_module "fix_proto"
 let fix_sub_ref = make_ref fixsub_module "Fix_sub"
 let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset name typ prop =
+let mkSubset evdref name typ prop =
   let open EConstr in
-  mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
+  mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
 let sigT = Lazy.from_fun build_sigma_type
 
 let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
-let rec telescope l =
+let rec telescope evdref l =
   let open EConstr in
   let open Vars in
   match l with
@@ -935,10 +938,8 @@ let rec telescope l =
 	  (fun (ty, tys, (k, constr)) decl ->
             let t = RelDecl.get_type decl in
             let pred = mkLambda (RelDecl.get_name decl, t, ty) in
-	    let ty = Universes.constr_of_global (Lazy.force sigT).typ in
-	    let ty = EConstr.of_constr ty in
-	    let intro = Universes.constr_of_global (Lazy.force sigT).intro in
-	    let intro = EConstr.of_constr intro in
+	    let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
+	    let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
 	    let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
 	      (sigty, pred :: tys, (succ k, intro)))
@@ -947,17 +948,15 @@ let rec telescope l =
       let (last, subst) = List.fold_right2
         (fun pred decl (prev, subst) ->
           let t = RelDecl.get_type decl in
-	  let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
-	  let p1 = EConstr.of_constr p1 in
-	  let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
-	  let p2 = EConstr.of_constr p2 in
+	  let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
+	  let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
 	  let proj1 = applist (p1, [t; pred; prev]) in
 	  let proj2 = applist (p2, [t; pred; prev]) in
 	    (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
 	(List.rev tys) tl (mkRel 1, [])
       in ty, (LocalDef (n, last, t) :: subst), constr
 
-  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
       ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
@@ -976,7 +975,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let top_env = push_rel_context binders_rel env in
   let top_arity = interp_type_evars top_env evdref arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
-  let argtyp, letbinders, make = telescope binders_rel in
+  let argtyp, letbinders, make = telescope evdref binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
@@ -1004,7 +1003,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       it_mkLambda_or_LetIn measure letbinders,
       it_mkLambda_or_LetIn measure binders
     in
-    let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+    let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
     let relargty = EConstr.of_constr relargty in
     let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
     let wf_rel_fun x y =
@@ -1012,15 +1011,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
  		     subst1 y measure_body |])
     in wf_rel, wf_rel_fun, measure
   in
-  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
+  let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
   let wfarg len = LocalAssum (Name argid',
-                              mkSubset (Name argid') argtyp
+                              mkSubset evdref (Name argid') argtyp
 				       (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
-  let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
+  let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
   let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1033,7 +1032,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
+    let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
@@ -1059,7 +1058,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let def =
-    mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
+    mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
 	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
@@ -1075,12 +1074,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
       let hook l gr _ = 
-	let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
+	let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let ty = EConstr.Unsafe.to_constr ty in
 	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
+	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -1097,10 +1096,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   let hook = Lemmas.mk_hook hook in
-  let fullcoqc = Evarutil.nf_evar !evdref def in
-  let fullctyp = Evarutil.nf_evar !evdref typ in
-  let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
-  let fullctyp = EConstr.Unsafe.to_constr fullctyp in
+  let fullcoqc = EConstr.to_constr !evdref def in
+  let fullctyp = EConstr.to_constr !evdref typ in
   Obligations.check_evars env !evdref;
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
@@ -1143,7 +1140,7 @@ let interp_recursive isfix fixl notations =
 	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
 	   let fixprot =
 	     try 
-	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
+	       let app = mkApp (fix_proto evdref, [|sort; t|]) in
 		 Typing.e_solve_evars env evdref app
 	     with e  when CErrors.noncritical e -> t
 	   in
@@ -1303,9 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns =
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
+      EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
     and typ =
-      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
+      EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
     in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index f57b1bba0..a678d20bb 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -453,11 +453,19 @@ let fold_left' f = function
     [] -> invalid_arg "fold_left'"
   | hd :: tl -> List.fold_left f hd tl
 
+let new_global sigma gr =
+  let open Sigma in
+  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+  in Sigma.to_evar_map sigma, c
+
+let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ())
+let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ())
+             
 let build_combined_scheme env schemes =
-  let defs = List.map (fun cst -> (* FIXME *)
-    let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
-      (c, Typeops.type_of_constant_in env c)) schemes in
-(*   let nschemes = List.length schemes in *)
+  let evdref = ref (Evd.from_env env) in
+  let defs = List.map (fun cst ->
+    let evd, c = Evd.fresh_constant_instance env !evdref cst in
+    evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in
   let find_inductive ty =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
@@ -471,26 +479,27 @@ let build_combined_scheme env schemes =
   let (c, t) = List.hd defs in
   let ctx, ind, nargs = find_inductive t in
   (* Number of clauses, including the predicates quantification *)
-  let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
-  let coqand  = Universes.constr_of_global @@ Coqlib.build_coq_and () in
-  let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in
+  let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
+  let sigma, coqand  = mk_coq_and !evdref in
+  let sigma, coqconj = mk_coq_conj sigma in
+  let () = evdref := sigma in
   let relargs = rel_vect 0 prods in
   let concls = List.rev_map
-    (fun (cst, t) -> (* FIXME *)
+    (fun (cst, t) ->
       mkApp(mkConstU cst, relargs),
       snd (decompose_prod_n prods t)) defs in
   let concl_bod, concl_typ =
     fold_left'
       (fun (accb, acct) (cst, x) ->
-	mkApp (coqconj, [| x; acct; cst; accb |]),
-	mkApp (coqand, [| x; acct |])) concls
+	mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]),
+	mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls
   in
   let ctx, _ =
     list_split_rev_at prods
       (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
-  (body, typ)
+  (!evdref, body, typ)
 
 let do_combined_scheme name schemes =
   let csts =
@@ -501,9 +510,9 @@ let do_combined_scheme name schemes =
                 with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
       schemes
   in
-  let body,typ = build_combined_scheme (Global.env ()) csts in
+  let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
   let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-  ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
+  ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index e5d79fd51..0f559d2bd 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit
 
 (** Combine a list of schemes into a conjunction of them *)
 
-val build_combined_scheme : env -> constant list -> constr * types
+val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
 
 val do_combined_scheme : Id.t located -> Id.t located list -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 405d37927..77be7f454 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1765,12 +1765,11 @@ let vernac_locate = let open Feedback in function
 let vernac_register id r =
  if Pfedit.refining () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let t = (Constrintern.global_reference (snd id)) in
-  if not (isConst t) then
+  let kn = Constrintern.global_reference (snd id) in
+  if not (isConstRef kn) then
     user_err Pp.(str "Register inline: a constant is expected");
-  let kn = destConst t in
   match r with
-  | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+  | RegisterInline -> Global.register_inline (destConstRef kn)
 
 (********************)
 (* Proof management *)