diff options
| author | aspiwack | 2008-06-27 15:27:30 +0000 |
|---|---|---|
| committer | aspiwack | 2008-06-27 15:27:30 +0000 |
| commit | 7b74581cd633d28c83589dff1adf060fcfe87e8a (patch) | |
| tree | 12f5ea9fc02682eb8945d5b7663a80a32c1ee69d | |
| 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
| -rw-r--r-- | proofs/logic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 654bc504a9..74c2a4befc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -53,7 +53,8 @@ let rec catchable_exception = function (* unification errors *) | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ - |CannotFindWellTypedAbstraction _)) -> true + |CannotFindWellTypedAbstraction _ + |UnsolvableImplicit _)) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not |