diff options
| author | gmelquio | 2011-04-28 14:29:16 +0000 |
|---|---|---|
| committer | gmelquio | 2011-04-28 14:29:16 +0000 |
| commit | ef2776e7de84cd324392f52fed2dfa72a44a97b1 (patch) | |
| tree | 2e7cc19dbc082477c042dd1b8d7f4ad7210815b6 /plugins/syntax/string_syntax.ml | |
| parent | f5276a11a40f86d5ed8ff14bd03d6ea71e7dad33 (diff) | |
Partial backtrack on the support for open terms in destruct/induction:
use type classes to possibly solve evars before trying to unify the
term (or the dependencies of its type) agains a subterm of the current
goal. This solves compatibility bug #2222. Mixing unification and type
classes is left for future work.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions