diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /tactics/refine.ml | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/refine.ml')
0 files changed, 0 insertions, 0 deletions