diff options
Diffstat (limited to 'kernel')
| -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 a69a98c1bf..a0b7d2cbce 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 308ff2bf3e..71169563b9 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 0cc91b430c..074139c9b4 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 |