Merge PR#678: [coqlib] Move `Coqlib` to `library/`.

4 files changed, 30 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e7b17991e3..c2c8065a98 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 42aaf3a227..af84b70a3d 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 7cee1e8a7e..45857df2ae 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 de485dbe84..8769c5659e 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