diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 617611bf..41fe8750 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *) +(* $Id: closure.ml 9215 2006-10-05 15:40:31Z herbelin $ *) open Util open Pp @@ -375,14 +375,17 @@ let defined_rels flags env = (rel_context 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 rec mind_equiv env (kn1,i1) (kn2,i2) = + let rec equiv kn1 kn2 = + kn1 = kn2 || + match (lookup_mind kn1 env).mind_equiv with + Some kn1' -> equiv kn2 kn1' + | None -> match (lookup_mind kn2 env).mind_equiv with + Some kn2' -> equiv kn2' kn1 + | None -> false in + i1 = i2 && equiv kn1 kn2 + +let mind_equiv_infos info = mind_equiv info.i_env let create mk_cl flgs env = { i_flags = flgs; |