From 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 25 Apr 2016 14:31:11 +0200
Subject: Fixing a "This clause is redundant" error when interpreting the "in"
 clause of a "match" over an irrefutable pattern.

---
 interp/constrintern.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'interp')

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')
-- 
cgit v1.2.3