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/cc/cctac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 201726d1e..b3017f359 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -26,7 +26,7 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) +let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) let _f_equal = reference ["Init";"Logic"] "f_equal" let _eq_rect = reference ["Init";"Logic"] "eq_rect" -- cgit v1.2.3