6 files changed, 151 insertions, 14 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/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/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.