diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.ml | 7 |
3 files changed, 8 insertions, 7 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 70f2f6b64a..71d952caf9 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -448,7 +448,7 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,NotClean _) as e -> raise e + | PretypeError (_,_,NotClean _) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/proofs/logic.ml b/proofs/logic.ml index 593ef0b329..5b55e1c02f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -48,13 +48,13 @@ open Pretype_errors let rec catchable_exception = function | Loc.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ + | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) | RefinerError _ | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* reduction errors *) | Tacred.ReductionTacticError _ (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _|OccurCheck _ |UnsolvableImplicit _)) -> true diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 677c739428..2802acfc1a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -395,11 +395,12 @@ let rec tclGOALBINDU s k = open Pretype_errors let rec catchable_exception = function | Loc.Exc_located(_,e) -> catchable_exception e - | Util.UserError _ | Type_errors.TypeError _ + | Util.UserError _ + | Type_errors.TypeError _ | PretypeError (_,_,TypingError _) | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true |