diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index bce564397c..93788ed422 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -196,6 +196,8 @@ let unfold_red kn = type table_key = id_key +let eq_table_key = Names.eq_id_key + type 'a infos = { i_flags : reds; i_repr : 'a infos -> constr -> 'a; @@ -250,18 +252,6 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -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 evars = { i_flags = flgs; i_repr = mk_cl; |