diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-25 14:31:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:45 +0200 |
| commit | 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 (patch) | |
| tree | 2f941e85d5cef3eba857291ed5ccf47d1385ed28 /interp | |
| parent | 0fc6d2dcdb7d12e37d43cbf44fecaf2c0fddadcc (diff) | |
Fixing a "This clause is redundant" error when interpreting the "in"
clause of a "match" over an irrefutable pattern.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 7 |
1 files changed, 4 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') |