10 files changed, 192 insertions, 17 deletions
diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v
deleted file mode 100644
index f62f6109e1..0000000000
--- a/test-suite/arithmetic/primitive.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Section S.
-  Variable A : Type.
-  Fail Primitive int : let x := A in Set := #int63_type.
-  Fail Primitive add := #int63_add.
-End S.
-
-(* [Primitive] should be forbidden in sections, otherwise its type after cooking
-will be incorrect:
-
-Check int.
-
-*)
diff --git a/test-suite/bugs/closed/bug_12534.v b/test-suite/bugs/closed/bug_12534.v
new file mode 100644
index 0000000000..a55515feb6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12534.v
@@ -0,0 +1,9 @@
+Record C {PROP: Prop} (P : PROP) : Type := { c : unit}.
+Check fun '{|c:=x|} => tt.      (* Fine *)
+Arguments Build_C {_ _} _.
+Check fun '(Build_C _) => tt. (* Works. Note: just 1 argument! *)
+Check fun '{|c:=x|} => tt.
+(* Error: The constructor @Build_C (in type @C) expects 1 argument. *)
+
+Set Asymmetric Patterns.
+Check fun '{|c:=x|} => tt.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 53ad8a9612..90a6a2ad96 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -80,6 +80,12 @@ NIL : list nat
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
+{|fun x : Z => x + x; 0|}
+     : Z
+{|op; 0; 1|}
+     : Z
+false = 0
+     : Prop
 Init.Nat.add
      : nat -> nat -> nat
 S
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 7d2f1e9ba8..d0b2f40f9c 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|].
 
 (**********************************************************************)
 (* Test recursive notations involving applications                    *)
-(* Caveat: does not work for applied constant because constants are   *)
-(* classified as notations for the particular constant while this     *)
-(* generic application notation is classified as generic              *)
+
+Module Application.
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+
+(* Application to a variable *)
+
 Check fun f => {| f; 0; 1; 2 |} : Z.
 
+(* Application to a fun *)
+
+Check {| (fun x => x+x); 0 |}.
+
+(* Application to a reference *)
+
+Axiom op : Z -> Z -> Z.
+Check {| op; 0; 1 |}.
+
+(* Interaction with coercion *)
+
+Axiom c : Z -> bool.
+Coercion c : Z >-> bool.
+Check false = {| c; 0 |}.
+
+End Application.
+
 (**********************************************************************)
 (* Check printing of notations from other modules *)
 
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 9cb019ca56..fa03ec8193 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -119,3 +119,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
+File "stdin", line 297, characters 0-30:
+Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
+0 :=: 0
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b3270d4f92..90d8da2bec 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -290,3 +290,11 @@ Check V tt.
 Check fun x : nat => V x.
 
 End O.
+
+Module Bug12691.
+
+Notation "x :=: y" := True (at level 70, no associativity, only parsing).
+Notation "x :=: y" := (x = y).
+Check (0 :=: 0).
+
+End Bug12691.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index ba316ceb64..b8db52735d 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -7,7 +7,7 @@ bli : Type
 Axioms:
 bli : Type
 Axioms:
-@seq relies on definitional UIP.
+seq relies on definitional UIP.
 Axioms:
 extensionality
   : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v
new file mode 100644
index 0000000000..b2d02a0c49
--- /dev/null
+++ b/test-suite/success/primitive.v
@@ -0,0 +1,69 @@
+(* This file mostly tests for the error paths in declaring primitives.
+   Successes are tested in the various test-suite/primitive/* directories *)
+
+(* [Primitive] should be forbidden in sections, otherwise its type
+after cooking will be incorrect. *)
+Section S.
+  Variable A : Type.
+  Fail Primitive int : let x := A in Set := #int63_type.
+  Fail Primitive int := #int63_type. (* we fail even if section variable not used *)
+End S.
+Section S.
+  Fail Primitive int := #int63_type. (* we fail even if no section variables *)
+End S.
+
+(* can't declare primitives with nonsense types *)
+Fail Primitive xx : nat := #int63_type.
+
+(* non-cumulative conversion *)
+Fail Primitive xx : Type := #int63_type.
+
+(* check evars *)
+Fail Primitive xx : let x := _ in Set := #int63_type.
+
+(* explicit type is unified with expected type, not just converted
+
+   extra universes are OK for monomorphic primitives (even though
+   their usefulness is questionable, there's no difference compared
+   with predeclaring them)
+ *)
+Primitive xx : let x := Type in _ := #int63_type.
+
+(* double declaration *)
+Fail Primitive yy := #int63_type.
+
+Module DoubleCarry.
+  (* XXX maybe should be an output test: this is the case where the new
+   declaration is already in the nametab so can be nicely printed *)
+  Module M.
+    Variant carry (A : Type) :=
+    | C0 : A -> carry A
+    | C1 : A -> carry A.
+
+    Register carry as kernel.ind_carry.
+  End M.
+
+  Module N.
+    Variant carry (A : Type) :=
+    | C0 : A -> carry A
+    | C1 : A -> carry A.
+
+    Fail Register carry as kernel.ind_carry.
+  End N.
+End DoubleCarry.
+
+(* univ polymorphic primitives *)
+
+(* universe count must be as expected *)
+Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type.
+
+(* use a phantom universe to ensure we check conversion not just the universe count *)
+Fail Primitive array@{u} : Set -> Set := #array_type.
+
+(* no constraints allowed! *)
+Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type.
+
+(* unification works for polymorphic primitives too (although universe
+   counts mean it's not enough) *)
+Fail Primitive array : let x := Type in _ -> Type := #array_type.
+Primitive array : _ -> Type := #array_type.
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index d3e2749088..3a6dfb1e11 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -171,6 +171,10 @@ End sFix.
 
 Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
 
+(* Check that VM/native properly keep the relevance of the predicate in the case info
+   (bad-relevance warning as error otherwise) *)
+Definition vm_rebuild_case := Eval vm_compute in eq_sind.
+
 Require Import ssreflect.
 
 Goal forall T : SProp, T -> True.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 7af09585d0..712cb6a135 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -15,6 +15,7 @@ Goal EQ nat 0 0.
 Hint Unfold EQ.
 auto.
 Qed.
+End toto.
 
 (* Check regular failure when statically existing ref does not exist
    any longer at run time *)
@@ -23,4 +24,71 @@ Goal let x := 0 in True.
 intro x.
 Fail (clear x; unfold x).
 Abort.
-End toto.
+
+(* Static analysis of unfold *)
+
+Module A.
+
+Opaque id.
+Ltac f := unfold id.
+Goal id 0 = 0.
+Fail f.
+Transparent id.
+f.
+Abort.
+
+End A.
+
+Module B.
+
+Module Type T. Axiom n : nat. End T.
+
+Module F(X:T).
+Ltac f := unfold X.n.
+End F.
+
+Module M. Definition n := 0. End M.
+Module N := F M.
+Goal match M.n with 0 => 0 | S _ => 1 end = 0.
+N.f.
+match goal with |- 0=0 => idtac end.
+Abort.
+
+End B.
+
+Module C.
+
+(* We reject inductive types and constructors *)
+
+Fail Ltac g := unfold nat.
+Fail Ltac g := unfold S.
+
+End C.
+
+Module D.
+
+(* In interactive mode, we delay the interpretation of short names *)
+
+Notation x := Nat.add.
+
+Goal let x := 0 in x = 0+0.
+unfold x.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let x := 0 in x = 0+0.
+intro; unfold x. (* dynamic binding (but is it really the most natural?) *)
+match goal with |- 0 = 0+0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+unfold fst.
+match goal with |- 0 = 0 => idtac end.
+Abort.
+
+Goal let fst := 0 in fst = Datatypes.fst (0,0).
+intro; unfold fst. (* dynamic binding *)
+match goal with |- 0 = Datatypes.fst (0,0) => idtac end.
+Abort.
+
+End D.