diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 6ef3d11da..8b4d02e04 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -194,7 +194,7 @@ val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> Reduction.conv_pb -> constr -> constr -> bool val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool -val eq_constr : constr -> constr -> bool +val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr |