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/firstorder/rules.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 86a677007..8c6b5b91d 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -231,7 +231,8 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str +let constant str = Universes.constr_of_global + @@ Coqlib.coq_reference "User" ["Init";"Logic"] str let defined_connectives=lazy [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not"))); -- cgit v1.2.3