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

4 files changed, 30 insertions, 19 deletions

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