diff options
| -rw-r--r-- | interp/constrintern.ml | 7 | ||||
| -rw-r--r-- | pretyping/cases.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/CaseInClause.v | 4 |
3 files changed, 10 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 434f765d0..072af0779 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1532,9 +1532,10 @@ let internalize globalenv env allow_patvar lvar c = (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = - (Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) - GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)) (* "=> _" *) in - Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,[main_sub_eqn;catch_all_sub_eqn])) + if List.for_all (irrefutable globalenv) thepats then [] else + [Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) + GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)] (* "=> _" *) in + Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in GCases (loc, sty, rtnpo, tms, List.flatten eqns') diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 257d1e578..d7fff8af4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -32,6 +32,8 @@ val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> ' val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a +val irrefutable : env -> cases_pattern -> bool + (** {6 Compilation primitive. } *) val compile_cases : diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 3679eead7..599b9566c 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -20,3 +20,7 @@ Theorem foo : forall (n m : nat) (pf : n = m), match pf in _ = N with | eq_refl => unit end. + +(* Check redundant clause is removed *) +Inductive I : nat * nat -> Type := C : I (0,0). +Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. |