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

2 files changed, 14 insertions, 19 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cbd8a7f0fe..5273eb3b50 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 e8c9f4ebaa..b0db2839be 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))))