Remove various circumvolutions from reduction behaviors

Incidentally, this fixes #10056

7 files changed, 226 insertions, 190 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 120b4e6f00..85e6f51387 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -90,48 +90,43 @@ module ReductionBehaviour = struct
   open Names
   open Libobject
 
-  type t = {
-    b_nargs: int;
-    b_recargs: int list;
-    b_dont_expose_case: bool;
-  }
+  type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags
+  and when_flags = { recargs : int list ; nargs : int option }
+
+  let more_args_when k { recargs; nargs } =
+    { nargs = Option.map ((+) k) nargs;
+      recargs = List.map ((+) k) recargs;
+    }
+
+  let more_args k = function
+    | NeverUnfold -> NeverUnfold
+    | UnfoldWhen x -> UnfoldWhen (more_args_when k x)
+    | UnfoldWhenNoMatch x -> UnfoldWhenNoMatch (more_args_when k x)
 
   let table =
     Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour"
 
-  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
-  type req =
-    | ReqLocal
-    | ReqGlobal of GlobRef.t * (int list * int * flag list)
-
   let load _ (_,(_,(r, b))) =
     table := GlobRef.Map.add r b !table
 
   let cache o = load 1 o
 
-  let classify = function
-    | ReqLocal, _ -> Dispose
-    | ReqGlobal _, _ as o -> Substitute o
+  let classify (local,_ as o) = if local then Dispose else Substitute o
 
-  let subst (subst, (_, (r,o as orig))) =
-    ReqLocal,
-    let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
+  let subst (subst, (local, (r,o) as orig)) =
+    let r' = subst_global_reference subst r in if r==r' then orig
+    else (local,(r',o))
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
+    | _,(false, (gr, b)) ->
       let b =
         if Lib.is_in_section gr then
           let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
-          let nargs' =
-             if b.b_nargs = max_int then max_int
-             else if b.b_nargs < 0 then b.b_nargs
-             else b.b_nargs + extra in
-          let recargs' = List.map ((+) extra) b.b_recargs in
-          { b with b_nargs = nargs'; b_recargs = recargs' }
+          more_args extra b
         else b
       in
-      Some (ReqGlobal (gr, req), (ConstRef c, b))
+      Some (false, (gr, b))
     | _ -> None
 
   let rebuild = function
@@ -148,55 +143,45 @@ module ReductionBehaviour = struct
 			rebuild_function = rebuild;
 		      }
 
-  let set local r (recargs, nargs, flags as req) =
-    let nargs = if List.mem `ReductionNeverUnfold flags then max_int else nargs in
-    let behaviour = {
-      b_nargs = nargs; b_recargs = recargs;
-      b_dont_expose_case = List.mem `ReductionDontExposeCase flags } in
-    let req = if local then ReqLocal else ReqGlobal (r, req) in
-    Lib.add_anonymous_leaf (inRedBehaviour (req, (r, behaviour)))
-  ;;
+  let set ~local r b =
+    Lib.add_anonymous_leaf (inRedBehaviour (local, (r, b)))
 
-  let get r =
-    try
-      let b = GlobRef.Map.find r !table in
-      let flags =
-	if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
-	else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
-      Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags)
-    with Not_found -> None
+  let get r = GlobRef.Map.find_opt r !table
 
   let print ref =
     let open Pp in
     let pr_global = Nametab.pr_global_env Id.Set.empty in
     match get ref with
     | None -> mt ()
-    | Some (recargs, nargs, flags) ->
-       let never = List.mem `ReductionNeverUnfold flags in
-       let nomatch = List.mem `ReductionDontExposeCase flags in
-       let pp_nomatch = spc() ++ if nomatch then
-				   str "but avoid exposing match constructs" else str"" in
-       let pp_recargs = spc() ++ str "when the " ++
+    | Some b ->
+       let pp_nomatch = spc () ++ str "but avoid exposing match constructs" in
+       let pp_recargs recargs = spc() ++ str "when the " ++
 			  pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++
 			  str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
 			  str " to a constructor" in
-       let pp_nargs =
-	 spc() ++ str "when applied to " ++ int nargs ++
-	   str (String.plural nargs " argument") in
-       hov 2 (str "The reduction tactics " ++
-		 match recargs, nargs, never with
-		 | _,_, true -> str "never unfold " ++ pr_global ref
-		 | [], 0, _ -> str "always unfold " ++ pr_global ref
-		 | _::_, n, _ when n < 0 ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-		 | _::_, n, _ when n > List.fold_left max 0 recargs ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++
-		      str " and" ++ pp_nargs ++ pp_nomatch
-		 | _::_, _, _ ->
-		    str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
-		 | [], n, _ when n > 0 ->
-		    str "unfold " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
-		 | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch )
+       let pp_nargs nargs =
+         spc() ++ str "when applied to " ++ int nargs ++
+         str (String.plural nargs " argument") in
+       let pp_when = function
+         | { recargs = []; nargs = Some 0 } ->
+           str "always unfold " ++ pr_global ref
+         | { recargs = []; nargs = Some n } ->
+           str "unfold " ++ pr_global ref ++ pp_nargs n
+         | { recargs = []; nargs = None } ->
+           str "unfold " ++ pr_global ref
+         | { recargs; nargs = Some n } when n > List.fold_left max 0 recargs ->
+           str "unfold " ++ pr_global ref ++ pp_recargs recargs ++
+           str " and" ++ pp_nargs n
+         | { recargs; nargs = _ } ->
+           str "unfold " ++ pr_global ref ++ pp_recargs recargs
+       in
+       let pp_behavior = function
+         | NeverUnfold -> str "never unfold " ++ pr_global ref
+         | UnfoldWhen x -> pp_when x
+         | UnfoldWhenNoMatch x -> pp_when x ++ pp_nomatch
+       in
+       hov 2 (str "The reduction tactics " ++ pp_behavior b)
+
 end
 
 (** Machinery about stack of unfolded constants *)
@@ -928,6 +913,7 @@ let equal_stacks sigma (x, l) (y, l') =
 
 let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let open Context.Named.Declaration in
+  let open ReductionBehaviour in
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
@@ -974,37 +960,42 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
           else (* Looks for ReductionBehaviour *)
             match ReductionBehaviour.get (Globnames.ConstRef c) with
             | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
-            | Some (recargs, nargs, flags) ->
-              if (List.mem `ReductionNeverUnfold flags
-                  || (nargs > 0 && Stack.args_size stack < nargs))
-              then fold ()
-              else (* maybe unfolds *)
-              if List.mem `ReductionDontExposeCase flags then
-                let app_sk,sk = Stack.strip_app stack in
-                let (tm',sk'),cst_l' =
-                  whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
-                in
-                let rec is_case x = match EConstr.kind sigma x with
-                  | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
-                  | App (hd, _) -> is_case hd
-                  | Case _ -> true
-                  | _ -> false in
-                if equal_stacks sigma (x, app_sk) (tm', sk')
-                || Stack.will_expose_iota sk'
-                || is_case tm'
-                then fold ()
-                else whrec cst_l' (tm', sk' @ sk)
-              else match recargs with
-                |[] -> (* if nargs has been specified *)
-                  (* CAUTION : the constant is NEVER refold
-                                          (even when it hides a (co)fix) *)
-                  whrec cst_l (body, stack)
-                |curr::remains -> match Stack.strip_n_app curr stack with
-                              | None -> fold ()
-                              | Some (bef,arg,s') ->
-                                whrec Cst_stack.empty
-                                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
-         end
+            | Some behavior ->
+              begin match behavior with
+              | NeverUnfold -> fold ()
+              | (UnfoldWhen { nargs = Some n } |
+                 UnfoldWhenNoMatch { nargs = Some n } )
+                when Stack.args_size stack < n ->
+                fold ()
+              | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *)
+                  let app_sk,sk = Stack.strip_app stack in
+                  let (tm',sk'),cst_l' =
+                    whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
+                  in
+                  let rec is_case x = match EConstr.kind sigma x with
+                    | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+                    | App (hd, _) -> is_case hd
+                    | Case _ -> true
+                    | _ -> false in
+                  if equal_stacks sigma (x, app_sk) (tm', sk')
+                  || Stack.will_expose_iota sk'
+                  || is_case tm'
+                  then fold ()
+                  else whrec cst_l' (tm', sk' @ sk)
+              | UnfoldWhen { recargs } -> (* maybe unfolds *)
+                begin match recargs with
+                  |[] -> (* if nargs has been specified *)
+                    (* CAUTION : the constant is NEVER refold
+                                            (even when it hides a (co)fix) *)
+                    whrec cst_l (body, stack)
+                  |curr::remains -> match Stack.strip_n_app curr stack with
+                    | None -> fold ()
+                    | Some (bef,arg,s') ->
+                      whrec Cst_stack.empty
+                        (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
+                end
+              end
+        end
        | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
           let kargs = CPrimitives.kind p in
           let (kargs,o) = Stack.get_next_primitive_args kargs stack in
@@ -1015,41 +1006,45 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let npars = Projection.npars p in
-         if not tactic_mode then
-           let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
-	     whrec Cst_stack.empty stack'
-         else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
-	 | None ->
+       if not tactic_mode then
+         let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
+         whrec Cst_stack.empty stack'
+       else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
+         | None ->
            let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-	   let stack'', csts = whrec Cst_stack.empty stack' in
-	     if equal_stacks sigma stack' stack'' then fold ()
-	     else stack'', csts
-	 | Some (recargs, nargs, flags) ->
-	   if (List.mem `ReductionNeverUnfold flags
-	       || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1))))
-	   then fold ()
-	   else
-	     let recargs = List.map_filter (fun x -> 
-	       let idx = x - npars in 
-		 if idx < 0 then None else Some idx) recargs
-	     in
-	       match recargs with
-	       |[] -> (* if nargs has been specified *)
-		(* CAUTION : the constant is NEVER refold
-                   (even when it hides a (co)fix) *)
+           let stack'', csts = whrec Cst_stack.empty stack' in
+           if equal_stacks sigma stack' stack'' then fold ()
+           else stack'', csts
+         | Some behavior ->
+           begin match behavior with
+             | NeverUnfold -> fold ()
+             | (UnfoldWhen { nargs = Some n }
+               | UnfoldWhenNoMatch { nargs = Some n })
+               when Stack.args_size stack < n - (npars + 1) -> fold ()
+             | UnfoldWhen { recargs }
+             | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *)
+               let recargs = List.map_filter (fun x ->
+                   let idx = x - npars in
+                   if idx < 0 then None else Some idx) recargs
+               in
+               match recargs with
+               |[] -> (* if nargs has been specified *)
+                 (* CAUTION : the constant is NEVER refold
+                                  (even when it hides a (co)fix) *)
                  let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
-		   whrec Cst_stack.empty(* cst_l *) stack'
-	       | curr::remains -> 
-		 if curr == 0 then (* Try to reduce the record argument *)
-		   whrec Cst_stack.empty 
-		     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
-		 else
-		   match Stack.strip_n_app curr stack with
-		   | None -> fold ()
-		   | Some (bef,arg,s') ->
-		     whrec Cst_stack.empty 
-		       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
-				      Stack.append_app [|c|] bef,cst_l)::s'))
+                 whrec Cst_stack.empty(* cst_l *) stack'
+               | curr::remains ->
+                 if curr == 0 then (* Try to reduce the record argument *)
+                   whrec Cst_stack.empty
+                     (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack)
+                 else
+                   match Stack.strip_n_app curr stack with
+                   | None -> fold ()
+                   | Some (bef,arg,s') ->
+                     whrec Cst_stack.empty
+                       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
+                                      Stack.append_app [|c|] bef,cst_l)::s')
+           end)
 
     | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
       apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b5d3ff7627..aa39921ea2 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -21,13 +21,12 @@ exception Elimconst
 
 (** Machinery to customize the behavior of the reduction *)
 module ReductionBehaviour : sig
-  type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
 
-(** [set is_local ref (recargs, nargs, flags)] *)
-  val set :
-    bool -> GlobRef.t -> (int list * int * flag list) -> unit
-  val get :
-    GlobRef.t -> (int list * int * flag list) option
+  type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags
+  and when_flags = { recargs : int list ; nargs : int option }
+
+  val set : local:bool -> GlobRef.t -> t -> unit
+  val get : GlobRef.t -> t option
   val print : GlobRef.t -> Pp.t
 end
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bcc20a41b4..231219c9de 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -664,18 +664,38 @@ let whd_nothing_for_iota env sigma s =
    it fails if no redex is around *)
 
 let rec red_elim_const env sigma ref u largs =
+  let open ReductionBehaviour in
   let nargs = List.length largs in
   let largs, unfold_anyway, unfold_nonelim, nocase =
     match recargs ref with
     | None -> largs, false, false, false
-    | Some (_,n,f) when nargs < n || List.mem `ReductionNeverUnfold f -> raise Redelimination
-    | Some (x::l,_,_) when nargs <= List.fold_left max x l -> raise Redelimination
-    | Some (l,n,f) ->
-        let is_empty = match l with [] -> true | _ -> false in
-	  reduce_params env sigma largs l, 
-	  n >= 0 && is_empty && nargs >= n,
-          n >= 0 && not is_empty && nargs >= n,
-	  List.mem `ReductionDontExposeCase f
+    | Some NeverUnfold -> raise Redelimination
+    | Some (UnfoldWhen { nargs = Some n } | UnfoldWhenNoMatch { nargs = Some n })
+      when nargs < n -> raise Redelimination
+    | Some (UnfoldWhen { recargs = x::l } | UnfoldWhenNoMatch { recargs = x::l })
+      when nargs <= List.fold_left max x l -> raise Redelimination
+    | Some (UnfoldWhen { recargs; nargs = None }) ->
+      reduce_params env sigma largs recargs,
+      false,
+      false,
+      false
+    | Some (UnfoldWhenNoMatch { recargs; nargs = None }) ->
+      reduce_params env sigma largs recargs,
+      false,
+      false,
+      true
+    | Some (UnfoldWhen { recargs; nargs = Some n }) ->
+      let is_empty = List.is_empty recargs in
+      reduce_params env sigma largs recargs,
+      is_empty && nargs >= n,
+      not is_empty && nargs >= n,
+      false
+    | Some (UnfoldWhenNoMatch { recargs; nargs = Some n }) ->
+      let is_empty = List.is_empty recargs in
+      reduce_params env sigma largs recargs,
+      is_empty && nargs >= n,
+      not is_empty && nargs >= n,
+      true
   in
   try match reference_eval env sigma ref with
     | EliminationCases n when nargs >= n ->
@@ -737,6 +757,7 @@ and reduce_params env sigma stack l =
    a reducible iota/fix/cofix redex (the "simpl" tactic) *)
 
 and whd_simpl_stack env sigma =
+  let open ReductionBehaviour in
   let rec redrec s =
     let (x, stack) = decompose_app_vect sigma s in
     let stack = Array.to_list stack in
@@ -761,30 +782,30 @@ and whd_simpl_stack env sigma =
 	  with Redelimination -> s')
 
       | Proj (p, c) ->
-        (try 
-	   let unf = Projection.unfolded p in
-	     if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
-               let npars = Projection.npars p in
- 		 (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with
- 		 | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> 
-                   (* simpl never *) s'
-		 | false, Some (l, n, f) when not (List.is_empty l) ->
-		   let l' = List.map_filter (fun i -> 
-                     let idx = (i - (npars + 1)) in
-		       if idx < 0 then None else Some idx) l in
-		   let stack = reduce_params env sigma stack l' in
-                     (match reduce_projection env sigma p ~npars
-		       (whd_construct_stack env sigma c) stack 
-		      with
-		      | Reduced s' -> redrec (applist s')
-		      | NotReducible -> s')
- 		 | _ ->
-                   match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
-		   | Reduced s' -> redrec (applist s')
-		   | NotReducible -> s')
-	   else s'
-	 with Redelimination -> s')
-	  
+        (try
+           let unf = Projection.unfolded p in
+           if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+             let npars = Projection.npars p in
+             (match unf, get (ConstRef (Projection.constant p)) with
+              | false, Some NeverUnfold -> s'
+              | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs })
+                when not (List.is_empty recargs) ->
+                let l' = List.map_filter (fun i ->
+                    let idx = (i - (npars + 1)) in
+                    if idx < 0 then None else Some idx) recargs in
+                let stack = reduce_params env sigma stack l' in
+                (match reduce_projection env sigma p ~npars
+                         (whd_construct_stack env sigma c) stack
+                 with
+                 | Reduced s' -> redrec (applist s')
+                 | NotReducible -> s')
+              | _ ->
+                match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
+                | Reduced s' -> redrec (applist s')
+                            | NotReducible -> s')
+                 else s'
+               with Redelimination -> s')
+
       | _ -> 
         match match_eval_ref env sigma x stack with
 	| Some (ref, u) ->
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 7074ad2d41..3c1e27ba9d 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -27,7 +27,7 @@ Nat.sub : nat -> nat -> nat
 Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor and when applied to 2 arguments 
+  2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
@@ -35,7 +35,7 @@ Nat.sub : nat -> nat -> nat
 Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
-  2nd arguments evaluate to a constructor 
+  2nd arguments evaluate to a constructor
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 pf :
@@ -54,7 +54,7 @@ fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 fcomp is not universe polymorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
-The reduction tactics unfold fcomp when applied to 6 arguments 
+The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
@@ -75,7 +75,7 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat
 f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
-  5th arguments evaluate to a constructor 
+  5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
@@ -84,7 +84,7 @@ f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
-  6th arguments evaluate to a constructor 
+  6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
@@ -93,7 +93,7 @@ f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor 
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
      = forall v : unit, f 0 0 5 v 3 = 2
@@ -104,7 +104,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
-  7th arguments evaluate to a constructor 
+  7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
 forall w : r, w 3 true = tt
@@ -115,3 +115,13 @@ w 3 true = tt
      : Prop
 The command has indeed failed with message:
 Extra arguments: _, _.
+volatilematch : nat -> nat
+
+volatilematch is not universe polymorphic
+Argument scope is [nat_scope]
+The reduction tactics always unfold volatilematch
+  but avoid exposing match constructs
+volatilematch is transparent
+Expands to: Constant Arguments.volatilematch
+     = fun n : nat => volatilematch n
+     : nat -> nat
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 844f96aaa1..b909f1b64c 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -55,3 +55,12 @@ Arguments w  x%F y%B : extra scopes.
 Check (w $ $ = tt).
 Fail Arguments w  _%F _%B.
 
+Definition volatilematch (n : nat) :=
+  match n with
+  | O => O
+  | S p => p
+  end.
+
+Arguments volatilematch / n : simpl nomatch.
+About volatilematch.
+Eval simpl in fun n => volatilematch n.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3f0717666c..65c902202d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -62,7 +62,7 @@ Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor 
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
@@ -101,7 +101,7 @@ Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
-  3rd arguments evaluate to a constructor 
+  3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.myplus
 @myplus
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 388f6957cf..279d4f0935 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1231,16 +1231,13 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   let clear_implicits_flag = List.mem `ClearImplicits flags in
   let default_implicits_flag = List.mem `DefaultImplicits flags in
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
+  let nomatch_flag = List.mem `ReductionDontExposeCase flags in
 
   let err_incompat x y =
     user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
 
   if assert_flag && rename_flag then
     err_incompat "assert" "rename";
-  if Option.has_some nargs_for_red && never_unfold_flag then
-    err_incompat "simpl never" "/";
-  if never_unfold_flag && List.mem `ReductionDontExposeCase flags then
-    err_incompat "simpl never" "simpl nomatch";
   if clear_scopes_flag && extra_scopes_flag then
     err_incompat "clear scopes" "extra scopes";
   if clear_implicits_flag && default_implicits_flag then
@@ -1385,19 +1382,24 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
       (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args)
   in
 
-  let rec narrow = function
-    | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
-    | [] -> [] | _ :: tl -> narrow tl
-  in
-  let red_flags = narrow flags in
-  let red_modifiers_specified =
-    not (List.is_empty rargs) || Option.has_some nargs_for_red
-    || not (List.is_empty red_flags)
+  let red_behavior =
+    let open Reductionops.ReductionBehaviour in
+    match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with
+    | true, false, [], None -> Some NeverUnfold
+    | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch"
+    | true, _, _::_, _ -> err_incompat "simpl never" "!"
+    | true, _, _, Some _ -> err_incompat "simpl never" "/"
+    | false, false, [], None  -> None
+    | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red;
+                                               recargs = rargs;
+                                             })
+    | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red;
+                                                     recargs = rargs;
+                                                   })
   in
 
-  if not (List.is_empty rargs) && never_unfold_flag then
-    err_incompat "simpl never" "!";
 
+  let red_modifiers_specified = Option.has_some red_behavior in
 
   (* Actions *)
 
@@ -1424,8 +1426,8 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
     match sr with
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
-         section_local c
-         (rargs, Option.default ~-1 nargs_for_red, red_flags)
+         ~local:section_local c (Option.get red_behavior)
+
     | _ -> user_err
              (strbrk "Modifiers of the behavior of the simpl tactic "++
               strbrk "are relevant for constants only.")