From 6841c6db48d57911d3886057e1ca47a5aa161ca7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Feb 2016 01:35:00 +0100
Subject: [coqlib] Deprecate redundant Coqlib functions.

We remove redundant functions `coq_constant`, `gen_reference`, and
`gen_constant`.

This is a first step towards a lazy binding of libraries references.
We have also chosen to untangle `constr` from `Coqlib`, as how to
instantiate the reference (in particular wrt universes) is a
client-side issue. (The client may want to provide an `evar_map` ?)

c.f. #186
---
 plugins/funind/indfun_common.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ea985ddecd..257f02b70b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -469,13 +469,17 @@ exception ToShow of exn
 let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq")
+    EConstr.of_constr @@
+    Universes.constr_of_global @@
+      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl")
+    EConstr.of_constr @@
+    Universes.constr_of_global @@
+      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
@@ -486,7 +490,10 @@ let hrec_id = Id.of_string "hrec"
 let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
 let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
-let well_founded_ltof = function () ->  EConstr.of_constr (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+
+let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+    Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
+
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
-- 
cgit v1.2.3