Merge branch 'v8.6'

25 files changed, 497 insertions, 17 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1dfbb29ff0..b32071e802 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,7 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
 get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
 
 
@@ -281,6 +281,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
+	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
@@ -304,16 +305,19 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	    | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 	          -e 's/\s*0\.\s*//g' \
 		  -e 's/\s*[-+]nan\s*//g' \
 		  -e 's/\s*[-+]inf\s*//g' \
+		  -e 's/^[^a-zA-Z]*//' \
+	    | sort \
 	    > $$tmpoutput; \
-	  sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	  sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
 		-e 's/\s*0\.\s*//g' \
 		-e 's/\s*[-+]nan\s*//g' \
 		-e 's/\s*[-+]inf\s*//g' \
-       	       $*.out > $$tmpexpected; \
+		-e 's/^[^a-zA-Z]*//' \
+	       $*.out | sort > $$tmpexpected; \
 	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v
index ef110ad0d0..5f80013df2 100644
--- a/test-suite/bugs/closed/3045.v
+++ b/test-suite/bugs/closed/3045.v
@@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) :=
     Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
   }.
 
-Arguments Compose {obj} [C s d d'] m1 m2 : rename.
+Arguments Compose {obj} [C s d d'] _ _ : rename.
 
 Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
 | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/closed/3753.v
index 05d77c831b..5bfbee9494 100644
--- a/test-suite/bugs/opened/3753.v
+++ b/test-suite/bugs/closed/3753.v
@@ -1,4 +1,4 @@
 Axiom foo : Type -> Type.
 Axiom bar : forall (T : Type), T -> foo T.
 Arguments bar A x : rename.
-Fail About bar.
+About bar.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v
new file mode 100644
index 0000000000..36efc42d47
--- /dev/null
+++ b/test-suite/bugs/closed/4471.v
@@ -0,0 +1,6 @@
+Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')),
+    @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b)))
+        (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))).
+Proof.
+  intros.
+  Fail generalize dependent (a, b).
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
new file mode 100644
index 0000000000..4ca6fe78cd
--- /dev/null
+++ b/test-suite/bugs/closed/4527.v
@@ -0,0 +1,267 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 1199 lines to 
+430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, 
+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) *)
+Inductive False := .
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Coq.Init.Datatypes.
+
+Import Coq.Init.Notations.
+
+Global Set Universe Polymorphism.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Inductive True : Type :=
+  I : True.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+Notation nat := Coq.Init.Datatypes.nat.
+Notation S := Coq.Init.Datatypes.S.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+
+Open Scope nat_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P 
+proj1_sig }.
+
+Notation sigT := sig (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in 
+Type@{i}.
+
+Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in
+                                        let ge := ((fun x => x) : Type1@{j} -> 
+Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left 
+associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : 
+type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : 
+function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Local Open Scope path_scope.
+
+Section EquivInverse.
+
+  Context {A B : Type} (f : A -> B) {feq : IsEquiv f}.
+
+  Theorem other_adj (b : B) : eissect f (f^-1 b) = ap f^-1 (eisretr f b).
+admit.
+Defined.
+
+  Global Instance isequiv_inverse : IsEquiv f^-1 | 10000
+    := BuildIsEquiv B A f^-1 f (eissect f) (eisretr f) other_adj.
+End EquivInverse.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+
+  Let issect' := fun x =>
+    ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+admit.
+Defined.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+
+End Adjointify.
+
+  Definition ExtensionAlong {A B : Type} (f : A -> B)
+             (P : B -> Type) (d : forall x:A, P (f x))
+    := { s : forall y:B, P y & forall x:A, s (f x) = d x }.
+
+  Fixpoint ExtendableAlong@{i j k l}
+           (n : nat) {A : Type@{i}} {B : Type@{j}}
+           (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := match n with
+         | 0 => Unit@{l}
+         | S n => (forall (g : forall a, C (f a)),
+                     ExtensionAlong@{i j k l l} f C g) *
+                  forall (h k : forall b, C b),
+                    ExtendableAlong n f (fun b => h b = k b)
+       end.
+
+  Definition ooExtendableAlong@{i j k l}
+             {A : Type@{i}} {B : Type@{j}}
+             (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := forall n, ExtendableAlong@{i j k l} n f C.
+
+Module Type ReflectiveSubuniverses.
+
+  Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                   Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+                               In@{u a i} O (O_reflector@{u a i} O T).
+
+  Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+
+  Parameter inO_equiv_inO@{u a i j k} :
+      forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+
+        let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+        let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+        In@{u a j} O U.
+
+  Parameter extendable_to_O@{u a i j k}
+  : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : 
+Type2le@{j a}} {Q_inO : In@{u a j} O Q},
+      ooExtendableAlong@{i i j k} (to O P) (fun _ => Q).
+
+End ReflectiveSubuniverses.
+
+Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
+Export Os.
+
+Existing Class In.
+
+  Coercion O_reflector : ReflectiveSubuniverse >-> Funclass.
+
+Arguments inO_equiv_inO {O} T {U} {_} f {_}.
+Global Existing Instance O_inO.
+
+Section ORecursion.
+  Context {O : ReflectiveSubuniverse}.
+
+  Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
+             (g h : O P -> Q) (p : g o to O P == h o to O P)
+  : g == h
+  := (fst (snd (extendable_to_O O 2) g h) p).1.
+
+  Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q}
+             (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P)
+  : O_indpaths g h p (to O P x) = p x
+  := (fst (snd (extendable_to_O O 2) g h) p).2 x.
+
+End ORecursion.
+
+Section Reflective_Subuniverse.
+  Universes Ou Oa.
+  Context (O : ReflectiveSubuniverse@{Ou Oa}).
+
+    Definition inO_isequiv_to_O (T:Type)
+    : IsEquiv (to O T) -> In O T
+    := fun _ => inO_equiv_inO (O T) (to O T)^-1.
+
+    Definition inO_to_O_retract (T:Type) (mu : O T -> T)
+    : Sect (to O T) mu -> In O T.
+    Proof.
+      unfold Sect; intros H.
+      apply inO_isequiv_to_O.
+      apply isequiv_adjointify with (g:=mu).
+      -
+ refine (O_indpaths (to O T o mu) idmap _).
+        intros x; exact (ap (to O T) (H x)).
+      -
+ exact H.
+    Defined.
+
+    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
+S)    : In@{Ou Oa i} O (x=y).
+    Proof.
+      simple refine (inO_to_O_retract@{i j} _ _ _); intro u.
+      -
+ assert (p : (fun _ : O (x=y) => x) == (fun _=> y)).
+        {
+ refine (O_indpaths _ _ _); simpl.
+          intro v; exact v.
+}
+        exact (p u).
+      -
+ hnf.
+        rewrite O_indpaths_beta; reflexivity.
+    Qed.
+    Check inO_paths@{Type Type}.
diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v
new file mode 100644
index 0000000000..03d2350a69
--- /dev/null
+++ b/test-suite/bugs/closed/4661.v
@@ -0,0 +1,10 @@
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : Type.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v
new file mode 100644
index 0000000000..8884812102
--- /dev/null
+++ b/test-suite/bugs/closed/4723.v
@@ -0,0 +1,28 @@
+
+Require Coq.Program.Tactics.
+
+Record Matrix (m n : nat).
+
+Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
+  Matrix (m*p) (n*q). Admitted.
+
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Ltac Obligation Tactic := admit.
+Fail Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+
+Axiom cheat : forall {A}, A.
+Obligation Tactic := apply cheat.
+
+Program Fact kp_assoc
+        (xr xc yr yc zr zc: nat)
+        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):
+  kp x (kp y z) = kp (kp x y) z.
+admit.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v
new file mode 100644
index 0000000000..7a87b07a8e
--- /dev/null
+++ b/test-suite/bugs/closed/4762.v
@@ -0,0 +1,24 @@
+Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q.
+
+Lemma foo P Q R : R = myand P Q -> P -> Q -> R.
+Proof. intros ->; constructor; auto. Qed.
+
+Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test1.
+Qed.
+
+Hint Extern 0 =>
+  match goal with
+  | |- myand _ _ => eapply foo; [reflexivity| |]
+  end : test2.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+  intros.
+  eauto with test2. (* works *)
+Qed.
+
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
new file mode 100644
index 0000000000..dbc3d46fce
--- /dev/null
+++ b/test-suite/bugs/closed/4798.v
@@ -0,0 +1,3 @@
+Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "8.4").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v
new file mode 100644
index 0000000000..6d21b66fe9
--- /dev/null
+++ b/test-suite/bugs/closed/4869.v
@@ -0,0 +1,18 @@
+Universes i.
+
+Fail Constraint i < Set.
+Fail Constraint i <= Set.
+Fail Constraint i = Set.
+Constraint Set <= i.
+Constraint Set < i.
+Fail Constraint i < j. (* undeclared j *)
+Fail Constraint i < Type. (* anonymous *)
+
+Set Universe Polymorphism.
+
+Section Foo.
+  Universe j.
+  Constraint Set < j.
+
+  Definition foo := Type@{j}.
+End Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v
new file mode 100644
index 0000000000..7e3c78dc2e
--- /dev/null
+++ b/test-suite/bugs/closed/4877.v
@@ -0,0 +1,12 @@
+Ltac induction_last :=
+  let v := match goal with
+           | |- forall x y, _ = _ -> _ => 1
+           | |- forall x y, _ -> _ = _ -> _ => 2
+           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
+           end in
+  induction v.
+
+Goal forall n m : nat, True -> n = m -> m = n.
+  induction_last.
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v
new file mode 100644
index 0000000000..c3043ca5d1
--- /dev/null
+++ b/test-suite/bugs/closed/5011.v
@@ -0,0 +1,2 @@
+Record decoder (n : nat) W := { decode : W -> nat }.
+Existing Class decoder.
diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v
new file mode 100644
index 0000000000..12c958be67
--- /dev/null
+++ b/test-suite/bugs/closed/5036.v
@@ -0,0 +1,10 @@
+Section foo.
+  Context (F : Type -> Type).
+  Context (admit : forall {T}, F T = True).
+  Hint Rewrite (fun T => @admit T).
+  Lemma bad : F False.
+  Proof.
+    autorewrite with core.
+    constructor.
+  Qed.
+End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v
new file mode 100644
index 0000000000..dc38738d8f
--- /dev/null
+++ b/test-suite/bugs/closed/5045.v
@@ -0,0 +1,3 @@
+Axiom silly : 1 = 1 -> nat -> nat.
+Goal forall pf : 1 = 1, silly pf 0 = 0 -> True.
+  Fail generalize (@eq nat).
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
index d79451f0f7..6611db70e2 100644
--- a/test-suite/output-modulo-time/ltacprof.v
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *)
 Ltac sleep' := do 100 (do 100 (do 100 idtac)).
 Ltac sleep := sleep'.
 
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out
new file mode 100644
index 0000000000..0cd5777ccf
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.out
@@ -0,0 +1,31 @@
+total time:      1.584s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+─sleep --------------------------------- 100.0% 100.0%       3    0.572s
+─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+└foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+
+total time:      1.584s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep --------------------------------- 100.0% 100.0%       3    0.572s
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+─foo1 ----------------------------------   0.0%  63.9%       1    1.012s
+─foo0 ----------------------------------   0.0%  31.3%       1    0.496s
+
+ tactic                                   local  total   calls       max 
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─foo2 ----------------------------------   0.0% 100.0%       1    1.584s
+ ├─foo1 --------------------------------   0.0%  63.9%       1    1.012s
+ │ ├─sleep -----------------------------  32.6%  32.6%       1    0.516s
+ │ └─foo0 ------------------------------   0.0%  31.3%       1    0.496s
+ │  └sleep -----------------------------  31.3%  31.3%       1    0.496s
+ └─sleep -------------------------------  36.1%  36.1%       1    0.572s
+
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
new file mode 100644
index 0000000000..50131470eb
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -0,0 +1,12 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+Require Coq.ZArith.BinInt.
+Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
+
+Ltac foo0 := idtac; sleep.
+Ltac foo1 := sleep; foo0.
+Ltac foo2 := sleep; foo1.
+Goal True.
+  foo2.
+  Show Ltac Profile CutOff 47.
+  constructor.
+Qed.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac631..bd9240476f 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3488cb3056..1633ad9765 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,20 @@
+File "stdin", line 1, characters 0-36:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
-The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T.
+File "stdin", line 2, characters 0-25:
+Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
+File "stdin", line 2, characters 0-25:
+Warning: This command is just asserting the number and names of arguments of
+identity. If this is what you want add ': assert' to silence the warning. If
+you want to clear implicit arguments add ': clear implicits'. If you want to
+clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
+File "stdin", line 4, characters 0-40:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -110,6 +121,9 @@ The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra argument y.
+File "stdin", line 53, characters 0-26:
+Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index b6fbeb6ec7..e42c983361 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
+Arguments identity T _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
 
 Module N : S with Module T := K := M
 
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a9862..5f30f7cda6 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
 Print Module N.
 
 End BAR.
+
+Module QUX.
+
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 590f6e191f..bb1cf06541 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -46,6 +46,25 @@ Module Backtracking.
   Qed.
   
   Unset Typeclasses Debug.
+
+  Module Leivant.
+    Axiom A : Type.
+    Existing Class A.
+    Axioms a b c d e: A.
+    
+    Ltac get_value H := eval cbv delta [H] in H.
+    
+    Goal True.
+      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
+    Admitted.
+
+    Goal exists x:A, x=a.
+      unshelve evar (t : A). all:cycle 1.
+      refine (@ex_intro _ _ t _).
+      all:cycle 1.
+      all:(typeclasses eauto + reflexivity).
+    Qed.      
+  End Leivant.
 End Backtracking.
 
 
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 91fb54d9a1..8681405175 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,7 +34,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; 1-2 : repeat idtac.
+  intros y; only 1-2 : repeat idtac.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.
@@ -44,12 +44,12 @@ Qed.
 Goal True /\ (True /\ True).
 Proof.
   dup.
-  - split; 2: (split; exact I).
+  - split; only 2: (split; exact I).
     exact I.
-  - split; 2: split; exact I.
+  - split; only 2: split; exact I.
 Qed.
 
 Goal True -> exists (x : Prop), x.
 Proof.
-  intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
index d4191b939b..2728672f30 100644
--- a/test-suite/success/simpl_tuning.v
+++ b/test-suite/success/simpl_tuning.v
@@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
 Abort. 
 
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 
 Lemma foo : volatile = volatile.
 simpl.