diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-27 15:27:30 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-27 15:27:30 +0000 |
| commit | 7b74581cd633d28c83589dff1adf060fcfe87e8a (patch) | |
| tree | 12f5ea9fc02682eb8945d5b7663a80a32c1ee69d /tactics/btermdn.mli | |
| parent | de877048b6a6fcd59315ae2c62a3036d16605e4c (diff) | |
Changement de catch_error pour qu'il rattrape les erreurs d'arguments
implicites. On peut désormais utiliser le fait que des arguments
implicites ne sont pas inférés pour backtracker dans des preuves. C'est
utile en particulier avec les typeclasses, mais peut servir dans
d'autres cas.
Le code suivant ne fait donc aucune erreur :
Definition toto {x:True} := True.
Goal True.
try apply toto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11183 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/btermdn.mli')
0 files changed, 0 insertions, 0 deletions