diff options
author | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:25:54 +0000 |
---|---|---|
committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:25:54 +0000 |
commit | 16b9b9d12313a84f8b29e998844188326d6b16f6 (patch) | |
tree | dde2a8a522c5693f47367f5ada4ec339cfd1249d | |
parent | b435eabdb5987e57071f32b8aca7306e9c5d53f3 (diff) |
Environ: generic equality on named_context replaced by named_context_equal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14330 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/sign.ml | 1 | ||||
-rw-r--r-- | kernel/sign.mli | 3 |
3 files changed, 5 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a69a98c1b..a0b7d2cbc 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -109,7 +109,7 @@ let lookup_named id env = Sign.lookup_named id env.env_named_context let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt let eq_named_context_val c1 c2 = - c1 == c2 || named_context_of_val c1 = named_context_of_val c2 + c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) diff --git a/kernel/sign.ml b/kernel/sign.ml index 308ff2bf3..71169563b 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -34,6 +34,7 @@ let rec lookup_named id = function | [] -> raise Not_found let named_context_length = List.length +let named_context_equal = list_equal eq_named_declaration let vars_of_named_context = List.map (fun (id,_,_) -> id) diff --git a/kernel/sign.mli b/kernel/sign.mli index 0cc91b430..074139c9b 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -23,6 +23,9 @@ val lookup_named : identifier -> named_context -> named_declaration (** number of declarations *) val named_context_length : named_context -> int +(** named context equality *) +val named_context_equal : named_context -> named_context -> bool + (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a |