Merge branch 'trunk' into pr379

24 files changed, 209 insertions, 28 deletions

diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 0000000000..b2f00ffc65
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+  bar mybase.
+  now_show (y = 0).
+  Undo 2.
+  foo mybase.
+  now_show (y = 0).
+Abort.
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a547685070..4b4f81dbce 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2c..8687eaab00 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1b..816bc845fd 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f0..c6fcc24b6b 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145d..64c7fd8eb1 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c9318..64dd8c304f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
\ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/closed/4969.v b/test-suite/bugs/closed/4969.v
new file mode 100644
index 0000000000..4dee41e221
--- /dev/null
+++ b/test-suite/bugs/closed/4969.v
@@ -0,0 +1,11 @@
+Require Import Classes.Init.
+
+Class C A := c : A.
+Instance nat_C : C nat := 0.
+Instance bool_C : C bool := true.
+Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
+Proof. auto. Qed.
+
+Goal True.
+  class_apply @silly; [reflexivity|].
+  reflexivity. Fail Qed.
diff --git a/test-suite/bugs/closed/5345.v b/test-suite/bugs/closed/5345.v
new file mode 100644
index 0000000000..d8448f35db
--- /dev/null
+++ b/test-suite/bugs/closed/5345.v
@@ -0,0 +1,7 @@
+Ltac break_tuple :=
+  match goal with
+  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    destruct a as [n m]
+  end.
diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v
new file mode 100644
index 0000000000..0118c18704
--- /dev/null
+++ b/test-suite/bugs/closed/5346.v
@@ -0,0 +1,29 @@
+Inductive comp : Type -> Type :=
+| Ret {T} : forall (v:T), comp T
+| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
+
+Notation "'do' x .. y <- p1 ; p2" :=
+  (Bind p1 (fun x => .. (fun y => p2) ..))
+    (at level 60, right associativity,
+     x binder, y binder).
+
+Definition Fst1 A B (p: comp (A*B)) : comp A :=
+  do '(a, b) <- p;
+    Ret a.
+
+Definition Fst2 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => Bind p (fun '(a, b) => Ret a)
+  end.
+
+Definition Fst3 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => do a <- p;
+          Ret (fst a)
+  end.
+
+Definition Fst A B (p: comp (A * B)) : comp A :=
+  match tt with
+  | _ => do '(a, b) <- p;
+          Ret a
+  end.
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
new file mode 100644
index 0000000000..2dc78d4c7f
--- /dev/null
+++ b/test-suite/bugs/closed/5372.v
@@ -0,0 +1,7 @@
+(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Function odd (n:nat) :=
+  match n with
+  | 0 => false
+  | S n => true
+  end
+with even (n:nat) := false.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index a2ee2d4c8e..979396969a 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -97,8 +97,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Unknown interpretation for notation "$".
+Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra arguments: _, _.
+Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index b084ad4984..4df21ae353 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -103,15 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Argument lists should agree on the names they provide.
+Argument lists should agree on the names they provide.
 The command has indeed failed with message:
-Error: Sequences of implicit arguments must be of different lengths.
+Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Some argument names are duplicated: F
+Some argument names are duplicated: F
 The command has indeed failed with message:
-Error: Argument z cannot be declared implicit.
+Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra arguments: y.
+Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 06a6b2d157..38d055b28e 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
-Error: Instance is not well-typed in the environment of ?x.
+Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index c6786c72ff..8d2a125c1d 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -16,4 +16,4 @@ Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
 In nested Ltac calls to "extensionality in (var)" and
 "clearbody (ne_var_list)", last call failed.
-Error: Hypothesis e depends on the body of H'
+Hypothesis e depends on the body of H'
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 26eaca8272..9d106d2dac 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-Error: x should not be bound in a recursive pattern of the right-hand side.
+x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
 The reference w was not found in the current environment.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-Error: z is expected to occur in binding position in the right-hand side.
+z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-Error: as y is a non-closed binder, no such "," is allowed to occur.
+as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Both ends of the recursive pattern are the same.
+Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 1ff09e3af6..35c3057d84 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,4 @@
 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
@@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 Hx
 nat
 nat
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
new file mode 100644
index 0000000000..172612405f
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing arguments for variables y and _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 0000000000..8ecd97aa56
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+  Fail foo.
+  Fail bar.
+  Fail bar True.
+  Fail baz.
+  Fail qux.
+  Fail mydo ltac:(fun _ _ => idtac).
+  Fail let tac := (fun _ => idtac) in tac.
+  Fail (fun _ => idtac).
+  Fail rec True.
+  Fail let rec tac x := tac in tac True.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 07bbb60c40..52acad7460 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -128,3 +128,10 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
+(* Check that we can have notations without any symbol iff they are "only printing". *)
+Fail Notation "" := (@nil).
+Notation "" := (@nil) (only printing).
+
+(* Check that a notation cannot be neither parsing nor printing. *)
+Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
index 58f79d45ec..e569bcb49f 100644
--- a/test-suite/success/decl_mode.v
+++ b/test-suite/success/decl_mode.v
@@ -153,7 +153,7 @@ proof.
       thus ~= (IZR (Zneg z) * IZR (Zneg z)).
   end cases.
 end proof.
-Qed.
+Admitted.
 
 Definition irrational (x:R):Prop :=
   forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q).
diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v
new file mode 100644
index 0000000000..f12b4d1f45
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac.v
@@ -0,0 +1,14 @@
+Definition x := 0.
+
+Hint Unfold x : mybase.
+
+Ltac autounfoldify base := autounfold with base.
+
+Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base.
+
+Goal x = 0.
+  progress autounfoldify mybase.
+  Undo.
+  progress autounfoldify_bis mybase.
+  trivial.
+Qed.
diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v
new file mode 100644
index 0000000000..f5c25540ef
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac_bis.v
@@ -0,0 +1,15 @@
+Parameter Foo : Prop.
+Axiom H : Foo.
+
+Hint Resolve H : mybase.
+
+Ltac foo base := eauto with base.
+
+Tactic Notation "bar" ident(base) :=
+  typeclasses eauto with base.
+
+Goal Foo.
+  progress foo mybase.
+  Undo.
+  progress bar mybase.
+Qed.
\ No newline at end of file
diff --git a/test-suite/success/ltac_match_pattern_names.v b/test-suite/success/ltac_match_pattern_names.v
new file mode 100644
index 0000000000..7363294960
--- /dev/null
+++ b/test-suite/success/ltac_match_pattern_names.v
@@ -0,0 +1,28 @@
+(* example from bug 5345 *)
+Ltac break_tuple :=
+  match goal with
+  | [ H: context[let '(n, m) := ?a in _] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    destruct a as [n m]
+  end.
+
+(* desugared version of break_tuple *)
+Ltac break_tuple' :=
+  match goal with
+  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
+    let n := fresh n in
+    let m := fresh m in
+    idtac
+  end.
+
+Ltac multiple_branches :=
+  match goal with
+  | [ H: match _ with
+         | left P => _
+         | right Q => _
+         end |- _ ] =>
+    let P := fresh P in
+    let Q := fresh Q in
+    idtac
+  end.
\ No newline at end of file