diff options
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 972b0b9e1..40c1ee082 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -201,7 +201,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe |