diff options
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r-- | pretyping/evd.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index d0a47fe96..b284bd42c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -515,11 +515,18 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map -(** This one forgets about the assignemts of universes. *) val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool +(** This one forgets about the assignemts of universes. *) + +val eq_constr : evar_map -> constr -> constr -> evar_map * bool +(** Syntactic equality up to universes, recording the associated constraints *) + +val e_eq_constr : evar_map ref -> constr -> constr -> bool +(** Syntactic equality up to universes. *) -(** Syntactic equality up to universe constraints. *) -val eq_constr : evar_map -> constr -> constr -> bool +val eq_constr_test : evar_map -> constr -> constr -> bool +(** Syntactic equality up to universes, throwing away the (consistent) constraints + in case of success. *) (******************************************************************** constr with holes *) |