diff options
| author | Hugo Herbelin | 2016-04-25 14:31:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:45 +0200 |
| commit | 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 (patch) | |
| tree | 2f941e85d5cef3eba857291ed5ccf47d1385ed28 | |
| parent | 0fc6d2dcdb7d12e37d43cbf44fecaf2c0fddadcc (diff) | |
Fixing a "This clause is redundant" error when interpreting the "in"
clause of a "match" over an irrefutable pattern.
| -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 434f765d06..072af07798 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 257d1e5787..d7fff8af4b 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 3679eead70..599b9566cb 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. |