diff options
| author | werner | 2005-10-27 16:19:39 +0000 |
|---|---|---|
| committer | werner | 2005-10-27 16:19:39 +0000 |
| commit | ad97cea6d32c0a5a58aca4355e2d40bb8a168575 (patch) | |
| tree | 723a47aaeb8adee4eb28d1d3f034e0d3f5f927ed | |
| parent | f92139a004d44c446fd7ac4d3c57a0901127b095 (diff) | |
catchable_exception laisse passer les InductiveError
BW
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7473 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 013cf227f5..0c9fe01195 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -54,9 +54,11 @@ let catchable_exception = function | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _| NoOccurrenceFound _ | CannotUnifyBindingType _|NotClean _))) | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true + Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + | Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ )))-> true | _ -> false + (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false |