diff options
| author | barras | 2001-06-27 16:47:38 +0000 |
|---|---|---|
| committer | barras | 2001-06-27 16:47:38 +0000 |
| commit | 9816d0201e8c72fb469706dd8739bec424a8ba5c (patch) | |
| tree | 6ef2874955d06450c04af836ee4eaa26cfcec8c3 /kernel/typeops.ml | |
| parent | 3266d96f6abd1d6ad84085a23c72cf5fa378f4f8 (diff) | |
commit d'un bug de Apply.
Avec Apply c, on essaie d'unifier le type de c avec le but courant.
Si ca echoue on essaie d'expanser la constante de tete du type du theoreme,
et essaie de faire Apply recursivement. Ca ameliore sensiblement la puissance
de Apply mais ce n'est pas 100% backward-compatible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions