Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"

8 files changed, 89 insertions, 3 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 8ce6f9795c..f064dfe763 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,18 +2,18 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | @k _ x0 => f x0 (F x0)
+  | k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
 Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
 proj = 
@@ -72,3 +72,11 @@ e1 : texp t1
 e2 : texp t2
 The term "0" has type "nat" while it is expected to have type
  "typeDenote t0".
+fun '{{n, m, _}} => n + m
+     : J -> nat
+fun '{{n, m, p}} => n + m + p
+     : J -> nat
+fun '(D n m p q) => n + m + p + q
+     : J -> nat
+The command has indeed failed with message:
+The constructor D (in type J) expects 3 arguments.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4074896420..6a4fd007df 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
   | TBinop t1 t2 _ b e1 e2 => O
   end.
 
+(* Test notations with local definitions in constructors *)
+
+Inductive J := D : forall n m, let p := n+m in nat -> J.
+Notation "{{ n , m , q }}" := (D n m q).
+
+Check fun x : J => let '{{n, m, _}} := x in n + m.
+Check fun x : J => let '{{n, m, p}} := x in n + m + p.
+
+(* Cannot use the notation because of the dependency in p *)
+
+Check fun x => let '(D n m p q) := x in n+m+p+q.
+
+(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
+
+Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index f4ecfd7362..ffea0819a5 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -105,3 +105,7 @@ tele (t : Type) '(y, z) (x : t0) := tt
          ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat))))))
 foo5 x nat x
      : nat -> nat
+fun x : ?A => x === x
+     : forall x : ?A, x = x
+where
+?A : [x : ?A |- Type] (x cannot be used)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 71536c68fb..250aecafd4 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -148,5 +148,15 @@ Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ].
 
 (* Cyprien's part of bug #4765 *)
 
+Section Bug4765.
+
 Notation foo5 x T y := (fun x : T => y).
 Check foo5 x nat x.
+
+End Bug4765.
+
+(**********************************************************************)
+(* Test printing of #5526                                             *)
+
+Notation "x === x" := (eq_refl x) (only printing, at level 10).
+Check (fun x => eq_refl x).
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 36d643a447..d45343fe60 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -14,3 +14,19 @@ build 5
      : test_r
 build_c 5
      : test_c
+fun '(C _ p) => p
+     : N -> True
+fun '{| T := T |} => T
+     : N -> Type
+fun '(C T p) => (T, p)
+     : N -> Type * True
+fun '{| q := p |} => p
+     : M -> True
+fun '{| U := T |} => T
+     : M -> Type
+fun '{| U := T; q := p |} => (T, p)
+     : M -> Type * True
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 6aa3df9830..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -19,3 +19,15 @@ Check build 5.
 Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
+
+Record N := C { T : Type; _ : True }.
+Check fun x:N => let 'C _ p := x in p.
+Check fun x:N => let 'C T _ := x in T.
+Check fun x:N => let 'C T p := x in (T,p).
+
+Record M := D { U : Type; a := 0; q : True }.
+Check fun x:M => let 'D T _ p := x in p.
+Check fun x:M => let 'D T _ p := x in T.
+Check fun x:M => let 'D T p := x in (T,p).
+Check fun x:M => let 'D T a p := x in (T,p,a).
+Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out
new file mode 100644
index 0000000000..e5520b8dfa
--- /dev/null
+++ b/test-suite/output/ShowMatch.out
@@ -0,0 +1,8 @@
+match # with
+ | f =>
+ end
+ 
+match # with
+ | A.f =>
+ end
+ 
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
new file mode 100644
index 0000000000..02b7eada83
--- /dev/null
+++ b/test-suite/output/ShowMatch.v
@@ -0,0 +1,13 @@
+(* Bug 5546 complained about unqualified constructors in Show Match output, 
+   when qualification is needed to disambiguate them
+*)
+
+Module A.
+  Inductive foo := f.
+  Show Match foo. (* no need to disambiguate *)
+End A. 
+
+Module B.
+  Inductive foo := f.
+  (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
+  Show Match A.foo.