diff options
| author | msozeau | 2009-07-09 15:32:28 +0000 |
|---|---|---|
| committer | msozeau | 2009-07-09 15:32:28 +0000 |
| commit | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (patch) | |
| tree | dc2517398ee4242e9656c7420a5eb5a3c101d82a /kernel/inductive.ml | |
| 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 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions