diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c44cf9980bf99..96a72f2085f90 100644
--- a/pretyping/tacred.ml
+++ b/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
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 6faf3f0269705..fb005def14504 100644
--- a/test-suite/success/simpl.v
+++ b/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.