diff options
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/term.ml b/checker/term.ml index 8d65bbe17..c39491ab5 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -487,9 +487,9 @@ let compare_constr f t1 t2 = f h1 h2 & List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> eq_constant c1 c2 - | Ind c1, Ind c2 -> c1 = c2 - | Construct c1, Construct c2 -> c1 = c2 + | Const c1, Const c2 -> eq_con_chk c1 c2 + | Ind c1, Ind c2 -> eq_ind_chk c1 c2 + | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> |