Remove various circumvolutions from reduction behaviors

Incidentally, this fixes #10056

3 files changed, 28 insertions, 9 deletions

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