Merge remote-tracking branch 'origin/master' into stm+doc_hook

9 files changed, 64 insertions, 34 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
diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
index 11c766b210..a26e683398 100644
--- a/test-suite/output/Error_msg_diffs.v
+++ b/test-suite/output/Error_msg_diffs.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* coq-prog-args: ("-color" "on" "-diffs" "on" "-async-proofs" "off") *)
 (* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
 (* Shows diffs in an error message for an "Unable to unify" error *)
 Require Import Arith List Bool.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 9d972a68f7..c1b9a2b1c6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,15 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+Entry constr:myconstr is
+[ "6" RIGHTA
+  [  ]
+| "5" RIGHTA
+  [ SELF;  "+"; NEXT ]
+| "4" RIGHTA
+  [ SELF;  "*"; NEXT ]
+| "3" RIGHTA
+  [  "<"; constr:operconstr LEVEL "10";  ">" ] ]
+
 [< b > + < b > * < 2 >]
      : nat
 [<< # 0 >>]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 81c64418cb..d1063bfd04 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
 Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
+Print Custom Grammar myconstr.
 
 Axiom a : nat.
 Notation b := a.
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
deleted file mode 100644
index 998eb37cc8..0000000000
--- a/test-suite/output/Quote.out
+++ /dev/null
@@ -1,24 +0,0 @@
-(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx))
-(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-   (f_and (f_const A)
-      (f_and (f_or (f_atom End_idx) (f_const A))
-         (f_or (f_const A) (f_not (f_atom End_idx))))))
-1 subgoal
-  
-  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
-      B
-  ============================
-  interp_f
-    (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
-    (f_and (f_atom (Left_idx End_idx))
-       (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
-          (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
-1 subgoal
-  
-  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
-      B
-  ============================
-  interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-    (f_and (f_const A)
-       (f_and (f_or (f_atom End_idx) (f_const A))
-          (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out
new file mode 100644
index 0000000000..0ff151c8b4
--- /dev/null
+++ b/test-suite/output/bug_9370.out
@@ -0,0 +1,12 @@
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
+1 subgoal
+  
+  ============================
+  1 = 1
diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v
new file mode 100644
index 0000000000..a7f4b7c23e
--- /dev/null
+++ b/test-suite/output/bug_9370.v
@@ -0,0 +1,12 @@
+Require Import Reals.
+Open Scope R_scope.
+Goal 1/1=1.
+Proof.
+  field_simplify (1/1).
+Show.
+  field_simplify.
+Show.
+  field_simplify.
+Show.
+  reflexivity.
+Qed.