Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

14 files changed, 82 insertions, 24 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d478..2b828d382a 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
   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
                      end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -48,8 +50,8 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    (let b0 := b in
-     if b0 as b return (P b -> True)
+    let b0 := b in
+    (if b0 as b return (P b -> True)
      then fun _ : P true => Logic.I
      else fun _ : P false => Logic.I) x
 end
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5ebc2..a4d19d6930 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -72,8 +72,8 @@ Inductive B : Prop := AC : P b -> B.
 Definition f : B -> True.
 
 Proof.
-intros [].
-destruct b as [|] ; intros _ ; exact Logic.I.
+intros [x].
+destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 483a9ea792..9680d2bbff 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal0 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
 Existential 2 =
 ?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
-Existential 3 = ?e : [q : nat  n : nat  m : nat |- n = ?y] 
+Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
index 848abd0096..f738b0d091 100644
--- a/test-suite/output/Extraction_matchs_2413.out
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -4,7 +4,7 @@ let test1 b =
   b
 (** val test2 : bool -> bool **)
 
-let test2 b =
+let test2 _ =
   False
 (** val wrong_id : 'a1 hole -> 'a2 hole **)
 
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
new file mode 100644
index 0000000000..e912003f03
--- /dev/null
+++ b/test-suite/output/Inductive.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Last occurrence of "list'" must have "A" as 1st argument in
+ "A -> list' A -> list' (A * A)%type".
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
new file mode 100644
index 0000000000..8db8956e32
--- /dev/null
+++ b/test-suite/output/Inductive.v
@@ -0,0 +1,3 @@
+Fail Inductive list' (A:Set) : Set :=
+| nil' : list' A
+| cons' : A -> list' A -> list' (A*A).
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405af..c17c63e724 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
 For sig2: Argument A is implicit
 For exist2: Argument A is implicit
 For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+              _]
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab1c..26eaca8272 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T1 => match x with
-                    | NIL => NONE2
-                    | (_ :') t => SOME2 t
-                    end
-     : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+                   | NIL => NONE2
+                   | (_ :') t => SOME2 t
+                   end
+     : list ?T -> option (list ?T)
 where
-?T1 : [x : list ?T1  x1 : list ?T1  x0 := x1 : list ?T1 |- Type] (x, x1,
-      x0 cannot be used)
+?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
+     x0 cannot be used)
 s
      : s
 10
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 23f33081b4..66458543aa 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -16,3 +16,5 @@ extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Closed under the global context
 Closed under the global context
+Axioms:
+M.foo : False
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index f23bc49808..c2003816ca 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -94,3 +94,19 @@ Proof (false_positive.add_comm 5).
 
 Print Assumptions comm_plus5.
 (* Should answer : Closed under the global context *)
+
+(** Print Assumption and Include *)
+
+Module INCLUDE.
+
+Module M.
+Axiom foo : False.
+End M.
+
+Module N.
+Include M.
+End N.
+
+Print Assumptions N.foo.
+
+End INCLUDE.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f050a..98420409e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic
 Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
 For sigT: Argument A is implicit
 For existT: Argument A is implicit
 For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f2d1447785..576fbd7c0b 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n in ?y ?y0 : T n
+fun n : nat => let x := A n : T n in ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T0] 
+?y : [n : nat  x := A n : T n |- ?T -> T n] 
+?y0 : [n : nat  x := A n : T n |- ?T] 
 fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T0 -> T n] 
-?y0 : [n : nat |- ?T0] 
+?y : [n : nat |- ?T -> T n] 
+?y0 : [n : nat |- ?T] 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 0000000000..20e274e254
--- /dev/null
+++ b/test-suite/output/ltac.out
@@ -0,0 +1,5 @@
+The command has indeed failed with message:
+Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Ltac f x y z :=
+  symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
+   dependent z
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
new file mode 100644
index 0000000000..373b870b9f
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,27 @@
+(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
+Goal True.
+Fail let T := constr:((fun a b : nat => a+b) 1 1) in
+  lazymatch T with
+  | (fun x z => ?y) 1 1
+    => pose ((fun x _ => y) 1 1)
+  end.
+Abort.
+
+(* This should not raise a warning (see #4317) *)
+Goal True.
+assert (H:= eq_refl ((fun x => x) 1)).
+let HT := type of H in
+lazymatch goal with
+| H1 : HT |- _ => idtac
+end.
+Abort.
+
+Ltac f x y z :=
+  symmetry in x, y;
+  auto with z;
+  auto;
+  intros;
+  clearbody x;
+  generalize dependent z.
+
+Print Ltac f.