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/fourier/fourierR.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 25d8f8c832..d35e4ec6fa 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -285,7 +285,8 @@ let fourier_lineq lineq1 =
 let get = Lazy.force
 let cget = get
 let eget c = EConstr.of_constr (Lazy.force c)
-let constant = Coqlib.gen_constant "Fourier"
+let constant path s = Universes.constr_of_global @@
+  Coqlib.coq_reference "Fourier" path s
 
 (* Standard library *)
 open Coqlib
-- 
cgit v1.2.3