diff options
| author | Pierre-Marie Pédrot | 2016-11-29 17:49:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:44 +0100 |
| commit | 390fd4ac0a969103caeb5db3e5138e26f9a533de (patch) | |
| tree | f04f87b0fca81518797dabd0f9d2d395ba8ec2b8 /engine/evd.mli | |
| parent | d549d9d3d169fbfc5f555e3e4f22f46301161d53 (diff) | |
Chasing a few unsafe constr coercions.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 699b52c2b2..eeb9fd8618 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -569,19 +569,6 @@ val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr -(******************************************************************** - Conversion w.r.t. an evar map, not unifying universes. See - [Reductionops.infer_conv] for conversion up-to universes. *) - -val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** WARNING: This does not allow unification of universes *) - -val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool -(** Syntactic equality up to universes, recording the associated constraints *) - -val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool -(** Syntactic equality up to universes. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) |