diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 654cd2b1a..d18ee4fde 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -947,9 +947,12 @@ let base_sort_cmp pb s0 s1 = (* eq_constr extended with universe erasure *) let rec constr_cmp cv_pb t1 t2 = (match kind_of_term t1, kind_of_term t2 with - Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 - | _ -> false) - || compare_constr (constr_cmp cv_pb) t1 t2 + Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + constr_cmp Reduction.CONV t1 t2 & + constr_cmp cv_pb c1 c2 + | _ -> false) + || compare_constr (constr_cmp Reduction.CONV) t1 t2 let eq_constr = constr_cmp Reduction.CONV |