From 880a83169c1d1df8726d301a9f8a9fc845cc7d1e Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 21 Apr 2008 13:57:03 +0000 Subject: - Parameterize unification by two sets of transparent_state, one for open term unification (for constant and variable delta unfolding) and one to parameterize closed-term conversion. Most of the time conversion uses full delta and unification does no delta. This fine-grain is used in rewrite/setoid_rewrite, where only closed-term delta on global constants is allowed. - Interpret Hint Unfold as a directive for delta conversion in auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). - Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works correctly w.r.t. the old version regarding local definitions. - Fix closed bugs which needed updating due to syntax modifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/names.ml | 4 ++++ kernel/names.mli | 4 ++++ 2 files changed, 8 insertions(+) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 60b5b6e421..38eb38beaf 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -317,6 +317,10 @@ let hcons_names () = type transparent_state = Idpred.t * Cpred.t +let empty_transparent_state = (Idpred.empty, Cpred.empty) +let full_transparent_state = (Idpred.full, Cpred.full) +let var_full_transparent_state = (Idpred.full, Cpred.empty) + type 'a tableKey = | ConstKey of constant | VarKey of identifier diff --git a/kernel/names.mli b/kernel/names.mli index 64edf1702e..340f6e812f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -169,6 +169,10 @@ type 'a tableKey = type transparent_state = Idpred.t * Cpred.t +val empty_transparent_state : transparent_state +val full_transparent_state : transparent_state +val var_full_transparent_state : transparent_state + type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} of de Bruijn indice *) -- cgit v1.2.3