diff options
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 054057d1f..27848efa7 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -376,7 +376,12 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = eq_ind +let mind_equiv_infos info = mind_equiv info.i_env + +let eq_table_key k1 k2 = + match k1,k2 with + | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 + | _,_ -> k1=k2 let create mk_cl flgs env = { i_flags = flgs; |