Fixing coq#14207: multiple warning unused variable catching several c…

…ases.

pretyping/cases.ml

@@ -1638,6 +1638,9 @@ let matx_of_eqns env eqns =
       rhs = rhs }
   in List.map build_eqn eqns
 
+let reset_catch_all_vars matx =
+  List.iter (fun eqn -> eqn.catch_all_vars := []) matx
+
 (***************** Building an inversion predicate ************************)
 
 (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T"
@@ -2760,6 +2763,9 @@ let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predop
     | Some t -> typing_fun tycon env sigma t
     | None -> use_unit_judge env sigma in
 
+    (* catch_all warnings are by side effect; we reset the effect of the previous tries *)
+    reset_catch_all_vars matx;
+
     let pb =
       { env       = env;
         pred      = pred;

test-suite/output/Cases.out

@@ -232,3 +232,7 @@ match x with
 | @D' _ _ _ _ n _ p _ => (n, p)
 end
      : J' bool (true, true) -> nat * nat
+Warning: Unused variable s catches more than one case.
+[unused-pattern-matching-variable,pattern-matching]
+default is defined
+default is recursively defined (guarded on 1st argument)

test-suite/output/Cases.v

@@ -284,3 +284,27 @@ Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => e
 Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
 
 End ConstructorArgumentsNumber.
+
+Module OnlyOneWarning.
+
+Inductive type {base_type : Type} := base (t : base_type) | arrow (s d : type).
+Global Arguments type : clear implicits.
+Fixpoint interp {base_type} (base_interp : base_type -> Type) (t : type base_type) : Type
+  := match t with
+     | base t => base_interp t
+     | arrow s d => @interp _ base_interp s -> @interp _ base_interp d
+     end.
+Axiom admit : forall {T}, T.
+Section with_base.
+  Context {base_type : Type}
+          {base_interp : base_type -> Type}.
+  Local Notation type := (@type base_type).
+
+  Fixpoint default {t} : interp base_interp t
+    := match t with
+       | base x => admit
+       | arrow s d => fun _ => @default d
+       end.
+End with_base.
+
+End OnlyOneWarning.