Term: added function eq_named_declaration

We need to move eq_constr upwards

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14319 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 18 insertions, 12 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 91b32aea14..097b4db506 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -583,6 +583,18 @@ let compare_constr f t1 t2 =
       ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
   | _ -> false
 
+(*******************************)
+(*  alpha conversion functions *)
+(*******************************)
+
+(* alpha conversion : ignore print names and casts *)
+
+let rec eq_constr m n =
+  (m==n) or
+  compare_constr eq_constr m n
+
+let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
+
 (***************************************************************************)
 (*     Type of assumptions                                                 *)
 (***************************************************************************)
@@ -606,6 +618,9 @@ let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
 let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
 let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
 
+let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+  id_ord i1 i2 = 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+
 (***************************************************************************)
 (*     Type of local contexts (telescopes)                                 *)
 (***************************************************************************)
@@ -1089,18 +1104,6 @@ let rec isArity c =
   | Sort _          -> true
   | _               -> false
 
-(*******************************)
-(*  alpha conversion functions *)
-(*******************************)
-
-(* alpha conversion : ignore print names and casts *)
-
-let rec eq_constr m n =
-  (m==n) or
-  compare_constr eq_constr m n
-
-let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
-
 (*******************)
 (*  hash-consing   *)
 (*******************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 008cad9947..c40b6142af 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -354,6 +354,9 @@ val for_all_named_declaration :
 val for_all_rel_declaration :
   (constr -> bool) -> rel_declaration -> bool
 
+val eq_named_declaration :
+  named_declaration -> named_declaration -> bool
+
 (** {6 Contexts of declarations referred to by de Bruijn indices } *)
 
 (** In [rel_context], more recent declaration is on top *)