[coqlib] Move `Coqlib` to `library/`.

We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.

By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.

Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.

The main changes are:

- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
  have different needs with regards to universes/evar_maps, so we
  force them to call the (not very safe) `Universes.constr_of_global`
  explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
  `pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
  anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
  illustrates the danger of duplication in the code base; the solution
  chosen there was to transform the not-found anomaly into an error
  message, however the general policy was far from clear. The long
  term solution is indeed make `find_reference` emit `Not_found` and
  let the client handle the error maybe non-fatally. (so they can test
  for constants.

29 files changed, 160 insertions, 180 deletions

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 1f7fbcbf6..bfa43cde1 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,8 +25,10 @@ echo $TRAVIS_PULL_REQUEST
 echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
-if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then
-    mathcomp_CI_BRANCH=options+remove_non_sync
+if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then
+
+    mathcomp_CI_BRANCH=coqlib-part-02
     mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
+
 fi
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d52c18462..bb6c2f660 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -108,6 +108,19 @@ In GOption:
   passed to workers, etc... As a consequence, the field
   `Goptions.optsync` has been removed.
 
+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.
+
+  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.
+
 ** Tactic API **
 
 - pf_constr_of_global now returns a tactic instead of taking a continuation.
diff --git a/engine/termops.ml b/engine/termops.ml
index 19e62f8e6..ca32c06a7 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1468,25 +1468,3 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
-
-(*******************************************)
-(* Functions to deal with impossible cases *)
-(*******************************************)
-let impossible_default_case = ref None
-
-let set_impossible_default_clause c = impossible_default_case := Some c
-
-let coq_unit_judge =
-  let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
-  let na1 = Name (Id.of_string "A") in
-  let na2 = Name (Id.of_string "H") in
-  fun () ->
-    match !impossible_default_case with
-    | Some fn -> 
-        let (id,type_of_id), ctx = fn () in
-	  make_judge id type_of_id, ctx
-    | None ->
-	(* In case the constants id/ID are not defined *)
-	make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
-                 (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), 
-       Univ.ContextSet.empty
diff --git a/engine/termops.mli b/engine/termops.mli
index fe6dfb0ce..58837ba03 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -275,10 +275,6 @@ val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) puns
 val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
 val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
 
-(** {6 Functions to deal with impossible cases } *)
-val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
-
 (** {5 Debug pretty-printers} *)
 
 open Evd
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 607af82a0..6d290a325 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -14,6 +14,5 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Coqlib
 Discharge
 Declare
diff --git a/interp/coqlib.ml b/library/coqlib.ml
index 9105bdd54..955ff4c08 100644
--- a/interp/coqlib.ml
+++ b/library/coqlib.ml
@@ -10,11 +10,9 @@ open CErrors
 open Util
 open Pp
 open Names
-open Term
 open Libnames
 open Globnames
 open Nametab
-open Smartlocate
 
 let coq = Nameops.coq_string (* "Coq" *)
 
@@ -26,10 +24,16 @@ type message = string
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
 let find_reference locstr dir s =
-  let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
-  try global_of_extended_global (Nametab.extended_global_of_path sp)
+  let dp = make_dir dir in
+  let sp = Libnames.make_path dp (Id.of_string s) in
+  try Nametab.global_of_path sp
   with Not_found ->
-    anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
+    (* Following bug 5066 we are more permissive with the handling
+       of not found errors here *)
+    user_err ~hdr:locstr
+      Pp.(str "cannot find " ++ Libnames.pr_path sp ++
+          str "; maybe library " ++ Libnames.pr_dirpath dp ++
+          str " has to be required first.")
 
 let coq_reference locstr dir s = find_reference locstr (coq::dir) s
 
@@ -37,14 +41,10 @@ let has_suffix_in_dirs dirs ref =
   let dir = dirpath (path_of_global ref) in
   List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
 
-let global_of_extended q =
-  try Some (global_of_extended_global q) with Not_found -> None
-
 let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
-  let all = Nametab.locate_extended_all qualid in
-  let all = List.map_filter global_of_extended all in
+  let all = Nametab.locate_all qualid in
   let all = List.sort_uniquize RefOrdered_env.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
@@ -61,9 +61,6 @@ let gen_reference_in_modules locstr dirs s =
 	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	   prlist_with_sep pr_comma pr_dirpath dirs)
 
-let gen_constant_in_modules locstr dirs s =
-  Universes.constr_of_global (gen_reference_in_modules locstr dirs s)
-
 (* For tactics/commands requiring vernacular libraries *)
 
 let check_required_library d =
@@ -91,10 +88,6 @@ let init_reference dir s =
   let d = coq::"Init"::dir in
   check_required_library d; find_reference "Coqlib" d s
 
-let init_constant dir s =
-  let d = coq::"Init"::dir in
-  check_required_library d; Universes.constr_of_global @@ find_reference "Coqlib" d s
-
 let logic_reference dir s =
   let d = coq::"Logic"::dir in
   check_required_library d; find_reference "Coqlib" d s
@@ -144,12 +137,6 @@ let make_con dir id = Globnames.encode_con dir (Id.of_string id)
 let id = make_con datatypes_module "idProp"
 let type_of_id = make_con datatypes_module "IDProp"
 
-let _ = Termops.set_impossible_default_clause 
-  (fun () -> 
-    let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in
-    let (_, u) = destConst c in
-      (c,mkConstU (type_of_id,u)), ctx)
-
 (** Natural numbers *)
 let nat_kn = make_ind datatypes_module "nat"
 let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
@@ -189,14 +176,14 @@ type coq_sigma_data = {
   typ   : global_reference }
 
 type coq_bool_data  = {
-  andb : constr;
-  andb_prop : constr;
-  andb_true_intro : constr}
+  andb : global_reference;
+  andb_prop : global_reference;
+  andb_true_intro : global_reference}
 
 let build_bool_type () =
-  { andb =  init_constant ["Datatypes"] "andb";
-    andb_prop =  init_constant ["Datatypes"] "andb_prop";
-    andb_true_intro =  init_constant ["Datatypes"] "andb_true_intro" }
+  { andb =  init_reference ["Datatypes"] "andb";
+    andb_prop =  init_reference ["Datatypes"] "andb_prop";
+    andb_true_intro =  init_reference ["Datatypes"] "andb_true_intro" }
 
 let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
 
@@ -239,7 +226,6 @@ type coq_inversion_data = {
 }
 
 let lazy_init_reference dir id = lazy (init_reference dir id)
-let lazy_init_constant dir id = lazy (init_constant dir id)
 let lazy_logic_reference dir id = lazy (logic_reference dir id)
 
 (* Leibniz equality on Type *)
@@ -302,7 +288,7 @@ let build_coq_inversion_jmeq_data () =
   inv_congr = Lazy.force coq_jmeq_congr_canonical }
 
 (* Specif *)
-let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
+let coq_sumbool  = lazy_init_reference ["Specif"] "sumbool"
 
 let build_coq_sumbool () = Lazy.force coq_sumbool
 
@@ -344,22 +330,22 @@ let build_coq_inversion_eq_true_data () =
   inv_congr = Lazy.force coq_eq_true_congr }
 
 (* The False proposition *)
-let coq_False  = lazy_init_constant ["Logic"] "False"
+let coq_False  = lazy_init_reference ["Logic"] "False"
 
 (* The True proposition and its unique proof *)
-let coq_True   = lazy_init_constant ["Logic"] "True"
-let coq_I      = lazy_init_constant ["Logic"] "I"
+let coq_True   = lazy_init_reference ["Logic"] "True"
+let coq_I      = lazy_init_reference ["Logic"] "I"
 
 (* Connectives *)
-let coq_not = lazy_init_constant ["Logic"] "not"
-let coq_and = lazy_init_constant ["Logic"] "and"
-let coq_conj = lazy_init_constant ["Logic"] "conj"
-let coq_or = lazy_init_constant ["Logic"] "or"
-let coq_ex = lazy_init_constant ["Logic"] "ex"
-let coq_iff = lazy_init_constant ["Logic"] "iff"
+let coq_not = lazy_init_reference ["Logic"] "not"
+let coq_and = lazy_init_reference ["Logic"] "and"
+let coq_conj = lazy_init_reference ["Logic"] "conj"
+let coq_or = lazy_init_reference ["Logic"] "or"
+let coq_ex = lazy_init_reference ["Logic"] "ex"
+let coq_iff = lazy_init_reference ["Logic"] "iff"
 
-let coq_iff_left_proj  = lazy_init_constant ["Logic"] "proj1"
-let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2"
+let coq_iff_left_proj  = lazy_init_reference ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
 
 (* Runtime part *)
 let build_coq_True ()  = Lazy.force coq_True
@@ -393,7 +379,5 @@ let coq_or_ref     = lazy (init_reference ["Logic"] "or")
 let coq_iff_ref    = lazy (init_reference ["Logic"] "iff")
 
 (* Deprecated *)
-let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
 let gen_reference = coq_reference
-let gen_constant  = coq_constant
 
diff --git a/interp/coqlib.mli b/library/coqlib.mli
index 49802089d..716d97c9d 100644
--- a/interp/coqlib.mli
+++ b/library/coqlib.mli
@@ -9,7 +9,6 @@
 open Names
 open Libnames
 open Globnames
-open Term
 open Util
 
 (** This module collects the global references, constructions and
@@ -50,7 +49,6 @@ val coq_reference : message -> string list -> string -> global_reference
 val check_required_library : string list -> unit
 
 (** Search in several modules (not prefixed by "Coq") *)
-val gen_constant_in_modules  : string->string list list-> string -> constr
 val gen_reference_in_modules : string->string list list-> string -> global_reference
 
 val arith_modules : string list list
@@ -72,6 +70,10 @@ val jmeq_module_name : string list
 
 val datatypes_module_name : string list
 
+(** Identity  *)
+val id : constant
+val type_of_id : constant
+
 (** Natural numbers *)
 val nat_path : full_path
 val glob_nat : global_reference
@@ -102,9 +104,9 @@ val glob_jmeq : global_reference
    at runtime. *)
 
 type coq_bool_data = {
-  andb : constr;
-  andb_prop : constr;
-  andb_true_intro : constr}
+  andb : global_reference;
+  andb_prop : global_reference;
+  andb_true_intro : global_reference}
 val build_bool_type : coq_bool_data delayed
 
 (** {6 For Equality tactics } *)
@@ -161,33 +163,33 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed
 val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
 (** Specif *)
-val build_coq_sumbool : constr delayed
+val build_coq_sumbool : global_reference delayed
 
 (** {6 ... } *)
 (** Connectives 
    The False proposition *)
-val build_coq_False : constr delayed
+val build_coq_False : global_reference delayed
 
 (** The True proposition and its unique proof *)
-val build_coq_True : constr delayed
-val build_coq_I : constr delayed
+val build_coq_True : global_reference delayed
+val build_coq_I : global_reference delayed
 
 (** Negation *)
-val build_coq_not : constr delayed
+val build_coq_not : global_reference delayed
 
 (** Conjunction *)
-val build_coq_and : constr delayed
-val build_coq_conj : constr delayed
-val build_coq_iff : constr delayed
+val build_coq_and : global_reference delayed
+val build_coq_conj : global_reference delayed
+val build_coq_iff : global_reference delayed
 
-val build_coq_iff_left_proj : constr delayed
-val build_coq_iff_right_proj : constr delayed
+val build_coq_iff_left_proj : global_reference delayed
+val build_coq_iff_right_proj : global_reference delayed
 
 (** Disjunction *)
-val build_coq_or : constr delayed
+val build_coq_or : global_reference delayed
 
 (** Existential quantifier *)
-val build_coq_ex : constr delayed
+val build_coq_ex : global_reference delayed
 
 val coq_eq_ref : global_reference lazy_t
 val coq_identity_ref : global_reference lazy_t
@@ -205,10 +207,5 @@ val coq_or_ref : global_reference lazy_t
 val coq_iff_ref : global_reference lazy_t
 
 (* Deprecated functions *)
-val coq_constant  : message -> string list -> string -> constr
-[@@ocaml.deprecated "Please use Coqlib.find_reference"]
-val gen_constant  : message -> string list -> string -> constr
-[@@ocaml.deprecated "Please use Coqlib.find_reference"]
 val gen_reference :  message -> string list -> string -> global_reference
 [@@ocaml.deprecated "Please use Coqlib.find_reference"]
-
diff --git a/library/library.mllib b/library/library.mllib
index df4f73503..6f433b77d 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -16,3 +16,4 @@ Goptions
 Decls
 Heads
 Keys
+Coqlib
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index d35e4ec6f..5cac3cbaf 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -291,9 +291,9 @@ let constant path s = Universes.constr_of_global @@
 (* Standard library *)
 open Coqlib
 let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (build_coq_False ())
-let coq_not = lazy (build_coq_not ())
-let coq_eq = lazy (build_coq_eq ())
+let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ())
+let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ())
+let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ())
 
 (* Rdefinitions *)
 let constant_real = constant ["Reals";"Rdefinitions"]
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 55d361e3d..f8c7f98f6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -409,9 +409,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = EConstr.of_constr (Coqlib.build_coq_False ()) in
-  let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in
-  let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in
+  let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in
+  let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in
+  let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1596,7 +1596,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> error "No tcc proof !!"
      | Value lemma -> EConstr.of_constr lemma
-     | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
+     | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ())
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 257f02b70..90a082d1e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -120,7 +120,8 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
 let find_reference sl s =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8c972cd7c..8eaa9b0f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) ->
+		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index eabad955e..00020609e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -54,7 +54,9 @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"]
 let arith_Lt = ["Arith";"Lt"]
 
 let coq_init_constant s =
-  EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s)
+  EConstr.of_constr (
+    Universes.constr_of_global @@
+    Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -1223,7 +1225,7 @@ let get_current_subgoals_types () =
 
 exception EmptySubgoals
 let build_and_l sigma l =
-  let and_constr =  Coqlib.build_coq_and () in
+  let and_constr =  Universes.constr_of_global @@ Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cbd8a7f0f..5273eb3b5 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,7 @@ 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 p in
+  let p = EConstr.of_constr @@ Universes.constr_of_global 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 +735,8 @@ let rewrite_except h =
 
 let refl_equal = 
   let coq_base_constant s =
-    Coqlib.gen_constant_in_modules "RecursiveDefinition"
+    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")
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e8c9f4eba..b0db2839b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -55,22 +55,16 @@ let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
 
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let lazy_find_reference dir s =
+  let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in
+  fun () -> Lazy.force gr
 
-let try_find_global_reference dir s =
-  let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
-    try Nametab.global_of_path sp
-    with Not_found -> 
-      anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
-
-let find_reference dir s =
-  let gr = lazy (try_find_global_reference dir s) in
-    fun () -> Lazy.force gr
+let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s
 
 type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
 let find_global dir s =
-  let gr = lazy (try_find_global_reference dir s) in
+  let gr = lazy (find_reference dir s) in
     fun (evd,cstrs) ->
       let sigma = Sigma.Unsafe.of_evar_map evd in
       let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
@@ -81,7 +75,7 @@ let find_global dir s =
 
 (** Global constants. *)
 
-let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
+let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq"
 let coq_eq = find_global ["Init"; "Logic"] "eq"
 let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
 let coq_all = find_global ["Init"; "Logic"] "all"
@@ -158,11 +152,11 @@ end) = struct
   let forall_relation = find_global morphisms "forall_relation"
   let pointwise_relation = find_global morphisms "pointwise_relation"
 
-  let forall_relation_ref = find_reference morphisms "forall_relation"
-  let pointwise_relation_ref = find_reference morphisms "pointwise_relation"
+  let forall_relation_ref = lazy_find_reference morphisms "forall_relation"
+  let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation"
 
   let respectful = find_global morphisms "respectful"
-  let respectful_ref = find_reference morphisms "respectful"
+  let respectful_ref = lazy_find_reference morphisms "respectful"
 
   let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
 
@@ -174,8 +168,8 @@ end) = struct
 
   let rewrite_relation_class = find_global relation_classes "RewriteRelation"
 
-  let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper"))
-  let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy"))
+  let proper_class = lazy (class_info (find_reference morphisms "Proper"))
+  let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
     
   let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
     
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 053bb6fa1..7497aae3c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -328,7 +328,6 @@ let selecti s m =
 module M =
 struct
 
-  open Coqlib
   open Constr
   open EConstr
 
@@ -356,8 +355,8 @@ struct
       ["LRing_normalise"]]
 
   let coq_modules =
-   init_modules @
-    [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules
+   Coqlib.(init_modules @
+    [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules)
 
   let bin_module = [["Coq";"Numbers";"BinNums"]]
 
@@ -375,8 +374,8 @@ struct
     * ZMicromega.v
     *)
 
-  let gen_constant_in_modules s m n = EConstr.of_constr (gen_constant_in_modules s m n)
-  let init_constant = gen_constant_in_modules "ZMicromega" init_modules
+  let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+  let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
   let r_constant = gen_constant_in_modules "ZMicromega" r_modules
@@ -1529,18 +1528,18 @@ let rec apply_ids t ids =
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
 let coq_Node = 
- lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
-   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node"))
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
 let coq_Leaf = 
- lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
-   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf"))
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
 let coq_Empty = 
- lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
-   [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty"))
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
 
 let coq_VarMap = 
-  lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
-     [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"))
+  lazy (gen_constant_in_modules "VarMap"
+     [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
  
 
 let rec dump_varmap typ m =
@@ -2059,8 +2058,8 @@ let micromega_order_changer cert env ff  =
         [
          ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
          ("__varmap", vm, Term.mkApp
-          (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap"
-	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|]));
+          (gen_constant_in_modules "VarMap"
+	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.New.pf_concl gl)));
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 8c3471a98..3a0d1dcbc 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -543,7 +543,7 @@ let nsatz lpol =
 
 let return_term t =
   let a =
-    mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in
+    mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in
   let a = EConstr.of_constr a in
   generalize [a]
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 334baec8d..27ce0103a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -196,7 +196,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let gen_constant_in_modules n m s = EConstr.of_constr (gen_constant_in_modules n m s)
+let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index f38ca85b6..fbed1df17 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -63,13 +63,13 @@ let coq_modules =
 let bin_module = [["Coq";"Numbers";"BinNums"]]
 let z_module = [["Coq";"ZArith";"BinInt"]]
 
-let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules
-let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
-let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module
-let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module
+let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
+let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x
+let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x
+let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x
 
 (* Logic *)
-let coq_refl_equal = lazy(init_constant  "eq_refl")
+let coq_refl_equal = lazy(init_constant "eq_refl")
 let coq_and = lazy(init_constant "and")
 let coq_not = lazy(init_constant "not")
 let coq_or = lazy(init_constant "or")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d84e62a93..0cb72cc3a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -229,7 +229,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c))
+  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -274,7 +274,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c))
+  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e7b17991e..c2c8065a9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -961,7 +961,6 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
   let k = length_of_tomatch_type_sign na t in
   (p+k,liftn_predicate (k-1) (p+1) ccl tms)
 
-
 let use_unit_judge evd =
   let j, ctx = coq_unit_judge () in
   let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42aaf3a22..af84b70a3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -42,6 +42,31 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_unification:=a);
 }
 
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+(* XXX: we would like to search for this with late binding
+   "data.id.type" etc... *)
+let impossible_default_case () =
+  let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+  let (_, u) = Term.destConst c in
+  Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx)
+
+let coq_unit_judge =
+  let open Environ in
+  let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
+  let na1 = Name (Id.of_string "A") in
+  let na2 = Name (Id.of_string "H") in
+  fun () ->
+    match impossible_default_case () with
+    | Some (id, type_of_id, ctx) ->
+      make_judge id type_of_id, ctx
+    | None ->
+      (* In case the constants id/ID are not defined *)
+      Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+        (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), 
+      Univ.ContextSet.empty
+
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
     if is_transparent_constant ts cst then
@@ -351,7 +376,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
   match ground_test with
     | Some result -> result
     | None ->
-	(* Until pattern-unification is used consistently, use nohdbeta to not
+      (* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta (fst ts) env evd term1 in
         let term2 = apprec_nohdbeta (fst ts) env evd term2 in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 7cee1e8a7..45857df2a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
       Evarsolve.unification_result
 (**/**)
 
+(** {6 Functions to deal with impossible cases } *)
+val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
diff --git a/pretyping/program.ml b/pretyping/program.ml
index de485dbe8..8769c5659 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -6,26 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open CErrors
 open Util
-open Names
 
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-
-let find_reference locstr dir s =
-  let dp = make_dir dir in
-  let sp = Libnames.make_path dp (Id.of_string s) in
-  try Nametab.global_of_path sp
-  with Not_found ->
-    user_err (str "Library " ++ Libnames.pr_dirpath dp ++
-      str " has to be required first.")
-
-let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
-let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
-
-let init_constant dir s () = coq_constant "Program" dir s
-let init_reference dir s () = coq_reference "Program" dir s
+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 = 
   let open EConstr in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 768d6860d..fe44559ed 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -20,7 +20,7 @@ module NamedDecl = Context.Named.Declaration
 (* Absurd *)
 
 let mk_absurd_proof t =
-  let build_coq_not () = EConstr.of_constr (build_coq_not ()) in
+  let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
   let id = Namegen.default_dependent_ident in
   mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
@@ -35,7 +35,7 @@ let absurd c =
     let t = j.Environ.utj_val in
     let tac =
     Tacticals.New.tclTHENLIST [
-      elim_type (EConstr.of_constr (build_coq_False ()));
+      elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
       Simple.apply (mk_absurd_proof t)
     ] in
     Sigma.Unsafe.of_pair (tac, sigma)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 641929a77..bda25d7f0 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -106,8 +106,8 @@ let solveNoteqBranch side =
 
 let make_eq () =
 (*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
-let build_coq_not () = EConstr.of_constr (build_coq_not ())
-let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ())
+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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f9f9b9dd7..0a68ff129 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -934,9 +934,9 @@ let build_selector env sigma dirn c ind special default =
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
-let build_coq_False () = EConstr.of_constr (build_coq_False ())
-let build_coq_True () = EConstr.of_constr (build_coq_True ())
-let build_coq_I () = EConstr.of_constr (build_coq_I ())
+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 rec build_discriminator env sigma dirn c = function
   | [] ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 31d610abd..cf534f13a 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -62,9 +62,10 @@ let constr_of_global g = lazy (Universes.constr_of_global g)
 (* Some pre declaration of constant we are going to use *)
 let bb = constr_of_global Coqlib.glob_bool
 
-let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
 
 let andb_true_intro = fun _ ->
+  Universes.constr_of_global
     (Coqlib.build_bool_type()).Coqlib.andb_true_intro
 
 let tt = constr_of_global Coqlib.glob_true
@@ -73,9 +74,9 @@ let ff = constr_of_global Coqlib.glob_false
 
 let eq = constr_of_global Coqlib.glob_eq
 
-let sumbool = Coqlib.build_coq_sumbool
+let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ())
 
-let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c = induction false None c None None
 
@@ -849,7 +850,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
             mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
-              mkApp(sumbool(),[|eqnm;mkApp (Coqlib.build_coq_not(),[|eqnm|])|])
+              mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
           )
         )
       )
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b21e80bef..885769143 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -472,7 +472,8 @@ let build_combined_scheme env schemes =
   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 = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+  let coqand  = Universes.constr_of_global @@ Coqlib.build_coq_and () in
+  let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in
   let relargs = rel_vect 0 prods in
   let concls = List.rev_map
     (fun (cst, t) -> (* FIXME *)