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

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