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

1 files changed, 14 insertions, 15 deletions

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)));