diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 463f6f21dd..2d30b2aa30 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -12,6 +12,7 @@ open Util open Pp open Term open Names +open Declarations open Environ open Esubst @@ -385,6 +386,15 @@ let defined_rels flags env = env ~init:(0,[]) (* else (0,[])*) + +let rec mind_equiv info kn1 kn2 = + kn1 = kn2 || + match (lookup_mind kn1 info.i_env).mind_equiv with + Some kn1' -> mind_equiv info kn2 kn1' + | None -> match (lookup_mind kn2 info.i_env).mind_equiv with + Some kn2' -> mind_equiv info kn2' kn1 + | None -> false + let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; |