diff options
| -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 013cf227f..0c9fe0119 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 |