diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
| commit | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (patch) | |
| tree | dc2517398ee4242e9656c7420a5eb5a3c101d82a /pretyping/typeclasses.mli | |
| parent | 2a596b2f6df4d884aaec99a519044036a4a81596 (diff) | |
Use the proper unification flags in e_exact. This makes exact fail a bit
more often but respects the spec better. The changes in the stdlib are
reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing
conversion with delta on open terms in that case).
Also fix a minor bug in typeclasses not seeing typeclass evars when
their type was a (defined) evar itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 833cec6d5..d5f5d6182 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -80,7 +80,7 @@ val bool_out : Dyn.t -> bool val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map -val is_class_evar : evar_info -> bool +val is_class_evar : evar_map -> evar_info -> bool val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs |