[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.

12 files changed, 51 insertions, 54 deletions

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)