Followup of coq#17993, fixes coq#18239: anomaly on triggering conditi…

…ons for simpl.

We ensure that there are enough arguments in the original applied
constant, in addition to ensuring enough arguments in the constant
that immediately surrounds a global mutual fixpoint.

This incidentally fixes a pre-coq#17993 bug.

pretyping/tacred.ml

@@ -233,7 +233,7 @@ let compute_fix_reversibility sigma labs args fix =
     labs;
   typed_reversible_args, nlam, nargs
 
-let check_fix_reversibility env sigma ref u labs args refs ((lv,i),_ as fix) =
+let check_fix_reversibility env sigma ref u minarg labs args refs ((lv,i),_ as fix) =
   let li, nlam, nargs = compute_fix_reversibility sigma labs args (mkFix fix) in
   let k = lv.(i) in
   let refolding_data = {
@@ -247,13 +247,13 @@ let check_fix_reversibility env sigma ref u labs args refs ((lv,i),_ as fix) =
       EliminationFix (n-p+1,(li,n))
 *)
       EliminationFix {
-        trigger_min_args = nlam;
+        trigger_min_args = max minarg nlam;
         refolding_target = ref;
         refolding_data;
         }
   else
     EliminationFix {
-        trigger_min_args = nlam - nargs + k + 1;
+        trigger_min_args = max minarg (nlam - nargs + k + 1);
         refolding_target = ref;
         refolding_data;
         }
@@ -321,11 +321,11 @@ let compute_consteval allowed_reds env sigma ref u =
           let nbfix = Array.length lv in
           (if nbfix = 1 then
             let names = [|Some (ref,u)|] in
-            try check_fix_reversibility env sigma ref u labs l names fix
+            try check_fix_reversibility env sigma ref u n labs l names fix
             with Elimconst -> NotAnElimination
           else
-            let labs, l, names = invert_names allowed_reds env sigma lastref lastu names i in
-            try check_fix_reversibility env sigma lastref lastu labs l names fix
+            let labs', l', names = invert_names allowed_reds env sigma lastref lastu names i in
+            try check_fix_reversibility env sigma lastref lastu n labs' l' names fix
             with Elimconst -> NotAnElimination)
       | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n
       | Case (_,_,_,_,_,d,_) -> srec env n labs lastref lastu true d

test-suite/success/simpl.v

@@ -189,3 +189,46 @@ match goal with [ |- g a c n = g a c n ] => idtac end.
 Abort.
 
 End WithLetMutual.
+
+Module IotaTrigger1.
+
+Definition a x := match x with true => tt | false => tt end.
+Definition b x (y : unit) := a x.
+Definition c x := b x tt.
+Eval simpl in a true.
+Eval simpl in b true.
+Eval simpl in c true.
+
+End IotaTrigger1.
+
+Module IotaTrigger2.
+
+Definition a x := match x with true => fun _ => tt | false => fun _ => tt end tt.
+Definition b x (y : unit) := a x.
+Definition c x := b x tt.
+Eval simpl in a true.
+Eval simpl in b true.
+Eval simpl in c true.
+
+End IotaTrigger2.
+
+Module IotaTrigger3.
+
+Fixpoint f_fix_fun n := match n with 0 => fun _ : unit => true | S n => f_fix_fun n end.
+Definition boo_fix_fun n := f_fix_fun n.
+Eval simpl in boo_fix_fun 2. (* fun _ : unit => true *)
+
+Fixpoint f_fix n := match n with 0 => fun _ : unit => true | S n => f_fix n end.
+Definition boo_fix n := f_fix n tt.
+Eval simpl in boo_fix 2. (* boo_fix 2 *) (* because we wouldn't refold in general if it were, say, boo_fix (S x) *)
+
+Fixpoint f_mutual_fix n := match n with 0 => fun _ : unit => true | S n => g n end
+with g n := match n with 0 => fun _ : unit => true | S n => f_mutual_fix n end.
+Definition boo_mutual_fix n := f_mutual_fix n tt.
+Eval simpl in boo_mutual_fix 2. (* boo_mutual_fix 2 *) (* by consistency with unary case? *)
+
+Definition f_case n := match n with 0 => fun _ : unit => true | S n => fun _ => true end.
+Definition boo_case n := f_case n tt.
+Eval simpl in boo_case 2. (* true *)
+
+End IotaTrigger3.