diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 22:26:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 22:26:18 +0200 |
| commit | d9736dae4168927f735ca4f60b61a83929ae4435 (patch) | |
| tree | 4afd85aee98945c458f210261ccc4265298e4475 /pretyping/evd.mli | |
| parent | f96dc97f48df5d0fdf252be5f28478a58be77961 (diff) | |
Be more conservative and keep the use of eq_constr in pretyping/ functions.
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 *) |