From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 12:13:04 +0200
Subject: Adding a fold_glob_constr_with_binders combinator.

Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.

Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
---
 test-suite/.csdp.cache         | Bin 89077 -> 89077 bytes
 test-suite/success/boundvars.v |   5 +++++
 2 files changed, 5 insertions(+)
 create mode 100644 test-suite/success/boundvars.v

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd3..b99d80e95f 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 0000000000..7b6696af8e
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,5 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
-- 
cgit v1.2.3


From b4936da085b19ad508346d8e07ce1e922ef79c2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 15:05:16 +0200
Subject: Using fold_glob_constr_with_binders to code bound_glob_vars.

To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.

This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
---
 test-suite/.csdp.cache         | Bin 89077 -> 89077 bytes
 test-suite/success/boundvars.v |   9 +++++++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95f..ba85286dd3 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
index 7b6696af8e..fafe272925 100644
--- a/test-suite/success/boundvars.v
+++ b/test-suite/success/boundvars.v
@@ -3,3 +3,12 @@
 
 Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
 
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.
-- 
cgit v1.2.3


From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 test-suite/success/transparent_abstract.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/success/transparent_abstract.v

(limited to 'test-suite')

diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 0000000000..ff4509c4a8
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+  split.
+  transparent_abstract exact I using foo.
+  let x := (eval hnf in foo) in constr_eq x I.
+  let x := constr:(ltac:(constructor) : True) in
+  let T := type of x in
+  let x := constr:(_ : by_transparent_abstract x) in
+  let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+  pose x as x'.
+  simpl in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+  hnf in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+  exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
-- 
cgit v1.2.3


From 9839375100365ea3bd28bfc2efdb701db7d83adb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 12:35:01 +0100
Subject: Test surgical use of beta-iota in the type of variables coming from
 pattern-matching for refine.

---
 test-suite/bugs/closed/5219.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5219.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 0000000000..f7cec1a0cf
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+   pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+  intro x; refine match x with
+                  | existT _ x' e' => _
+                  end.
+  lazymatch goal with
+  | [ H : _ = _ |- _ ] => idtac
+  end.
-- 
cgit v1.2.3


From 746066172b8ed508886feb20cee239920ca7a4c7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Apr 2017 17:33:51 +0200
Subject: Test for bug #5193: Uncaught exception
 Class_tactics.Search.ReachedLimitEx.

---
 test-suite/bugs/closed/5193.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/5193.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5193.v b/test-suite/bugs/closed/5193.v
new file mode 100644
index 0000000000..cc8739afe6
--- /dev/null
+++ b/test-suite/bugs/closed/5193.v
@@ -0,0 +1,14 @@
+Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
+
+Typeclasses eauto := debug.
+Set Typeclasses Debug Verbosity 2.
+
+Inductive Finx(n : nat) : Set :=
+| Fx1(i : nat)(e : n = S i)
+| FxS(i : nat)(f : Finx i)(e : n = S i).
+
+Context `{Finx_eqdec : forall n, Eqdec (Finx n)}.
+
+Goal {x : Type & Eqdec x}.
+  eexists.
+  try typeclasses eauto 1 with typeclass_instances.
-- 
cgit v1.2.3


From 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:30:45 +0200
Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with
 evars).

The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.

One day, evar kinds will need a little cleaning...
---
 test-suite/bugs/closed/5487.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/5487.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v
new file mode 100644
index 0000000000..9b995f4503
--- /dev/null
+++ b/test-suite/bugs/closed/5487.v
@@ -0,0 +1,9 @@
+(* Was a collision between an ltac pattern variable and an evar *)
+
+Goal forall n, exists m, n = m :> nat.
+Proof.
+  eexists.
+  Fail match goal with
+  | [ |- ?x = ?y ]
+    => match x with y => idtac end
+  end.
-- 
cgit v1.2.3


From db28e827d21658797418c320d566fb99570b44b6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:20:35 +0200
Subject: Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions
 with evars)."

One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:

~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~

Thank you!
---
 test-suite/bugs/closed/5487.v | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 test-suite/bugs/closed/5487.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v
deleted file mode 100644
index 9b995f4503..0000000000
--- a/test-suite/bugs/closed/5487.v
+++ /dev/null
@@ -1,9 +0,0 @@
-(* Was a collision between an ltac pattern variable and an evar *)
-
-Goal forall n, exists m, n = m :> nat.
-Proof.
-  eexists.
-  Fail match goal with
-  | [ |- ?x = ?y ]
-    => match x with y => idtac end
-  end.
-- 
cgit v1.2.3


From 12f1c409daf2cdbd7d0323f0d61723819532b362 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:56:25 +0200
Subject: Really fixing #2602 which was wrongly working because of #5487 hiding
 the cause.

The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
---
 test-suite/success/ltac.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..d7ec092d76 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,16 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* A variant of #2602 which was wrongly succeeding because "a", bound to
+   "?m", was then internally turned into a "_" in the second matching *)
+
+Goal exists m, S m > 0.
+eexists.
+Fail match goal with
+ | |- context [ S ?a ] =>
+     match goal with
+       | |- S a > a => idtac
+     end
+end.
+Abort.
-- 
cgit v1.2.3


From c3aec655a8a33fff676c79e12888d193cc2e237b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:58:38 +0200
Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with
 evars).

The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.

One day, evar kinds will need a little cleaning...

PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
---
 test-suite/bugs/closed/5487.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/5487.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v
new file mode 100644
index 0000000000..9b995f4503
--- /dev/null
+++ b/test-suite/bugs/closed/5487.v
@@ -0,0 +1,9 @@
+(* Was a collision between an ltac pattern variable and an evar *)
+
+Goal forall n, exists m, n = m :> nat.
+Proof.
+  eexists.
+  Fail match goal with
+  | [ |- ?x = ?y ]
+    => match x with y => idtac end
+  end.
-- 
cgit v1.2.3


From f6856c5022ef27cdc492daadd1301cfcad025b01 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 1 May 2017 11:34:00 -0400
Subject: remove unneeded -emacs flag to coq-prog-args

---
 test-suite/bugs/closed/3080.v                   | 2 +-
 test-suite/bugs/closed/3323.v                   | 2 +-
 test-suite/bugs/closed/3332.v                   | 2 +-
 test-suite/bugs/closed/3346.v                   | 2 +-
 test-suite/bugs/closed/3348.v                   | 2 +-
 test-suite/bugs/closed/3352.v                   | 2 +-
 test-suite/bugs/closed/3375.v                   | 2 +-
 test-suite/bugs/closed/3393.v                   | 2 +-
 test-suite/bugs/closed/3427.v                   | 2 +-
 test-suite/bugs/closed/3539.v                   | 2 +-
 test-suite/bugs/closed/3612.v                   | 2 +-
 test-suite/bugs/closed/3649.v                   | 2 +-
 test-suite/bugs/closed/3881.v                   | 2 +-
 test-suite/bugs/closed/3956.v                   | 2 +-
 test-suite/bugs/closed/4089.v                   | 2 +-
 test-suite/bugs/closed/4121.v                   | 2 +-
 test-suite/bugs/closed/4394.v                   | 2 +-
 test-suite/bugs/closed/4400.v                   | 2 +-
 test-suite/bugs/closed/4456.v                   | 2 +-
 test-suite/bugs/closed/4527.v                   | 2 +-
 test-suite/bugs/closed/4533.v                   | 2 +-
 test-suite/bugs/closed/4544.v                   | 2 +-
 test-suite/bugs/closed/4656.v                   | 2 +-
 test-suite/bugs/closed/4673.v                   | 2 +-
 test-suite/bugs/closed/4722.v                   | 2 +-
 test-suite/bugs/closed/4727.v                   | 2 +-
 test-suite/bugs/closed/4733.v                   | 2 +-
 test-suite/bugs/closed/4769.v                   | 2 +-
 test-suite/bugs/closed/4780.v                   | 2 +-
 test-suite/bugs/closed/4785_compat_85.v         | 2 +-
 test-suite/bugs/closed/4811.v                   | 2 +-
 test-suite/bugs/closed/4818.v                   | 2 +-
 test-suite/bugs/closed/5198.v                   | 2 +-
 test-suite/bugs/closed/HoTT_coq_012.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_032.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_053.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_054.v           | 1 -
 test-suite/bugs/closed/HoTT_coq_055.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_059.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_062.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_097.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_107.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_108.v           | 2 +-
 test-suite/bugs/closed/HoTT_coq_123.v           | 2 +-
 test-suite/bugs/opened/4803.v                   | 2 +-
 test-suite/output-modulo-time/ltacprof.v        | 2 +-
 test-suite/output-modulo-time/ltacprof_cutoff.v | 2 +-
 test-suite/output/ErrorInModule.v               | 2 +-
 test-suite/output/ErrorInSection.v              | 2 +-
 test-suite/success/Compat84.v                   | 2 +-
 50 files changed, 49 insertions(+), 50 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v
index 7d0dc090e1..36ab7ff599 100644
--- a/test-suite/bugs/closed/3080.v
+++ b/test-suite/bugs/closed/3080.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* -*- coq-prog-args: ("-nois") -*- *)
 Delimit Scope type_scope with type.
 Delimit Scope function_scope with function.
 
diff --git a/test-suite/bugs/closed/3323.v b/test-suite/bugs/closed/3323.v
index 22b1603b60..4622634eaa 100644
--- a/test-suite/bugs/closed/3323.v
+++ b/test-suite/bugs/closed/3323.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 297 lines to 117 lines, then from 95 lines to 79 lines, then from 82 lines to 68 lines *)
 
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v
index d86470cdee..a3564bfcce 100644
--- a/test-suite/bugs/closed/3332.v
+++ b/test-suite/bugs/closed/3332.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-time") -*- *)
+(* -*- coq-prog-args: ("-time") -*- *)
 Definition foo : True.
 Proof.
 Abort. (* Toplevel input, characters 15-21:
diff --git a/test-suite/bugs/closed/3346.v b/test-suite/bugs/closed/3346.v
index 638404f2cb..09bd789345 100644
--- a/test-suite/bugs/closed/3346.v
+++ b/test-suite/bugs/closed/3346.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a.
 (* This should fail with -indices-matter *)
 Fail Check paths nat O O : Prop.
diff --git a/test-suite/bugs/closed/3348.v b/test-suite/bugs/closed/3348.v
index d9ac09d8d3..904de68964 100644
--- a/test-suite/bugs/closed/3348.v
+++ b/test-suite/bugs/closed/3348.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Set Universe Polymorphism.
 Set Printing Universes.
 Inductive Empty : Set := .
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index f8113e4c78..555accfd51 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty"
 Defined.
 
 Module B.
-(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *)
 Set Universe Polymorphism.
 Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
diff --git a/test-suite/bugs/closed/3375.v b/test-suite/bugs/closed/3375.v
index d7ce02ea87..1e0c8e61f4 100644
--- a/test-suite/bugs/closed/3375.v
+++ b/test-suite/bugs/closed/3375.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-impredicative-set") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *)
 
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v
index f7ab5f76a5..ae8e41e29e 100644
--- a/test-suite/bugs/closed/3393.v
+++ b/test-suite/bugs/closed/3393.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *)
 Set Universe Polymorphism.
 Axiom admit : forall {T}, T.
diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v
index 374a53928d..9a57ca7703 100644
--- a/test-suite/bugs/closed/3427.v
+++ b/test-suite/bugs/closed/3427.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *)
 Generalizable All Variables.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v
index d258bb31f8..b0c4b23702 100644
--- a/test-suite/bugs/closed/3539.v
+++ b/test-suite/bugs/closed/3539.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *)
 (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0
    coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *)
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a547685070..90182a4881 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \
 lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2c..367d380ec3 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* -*- coq-prog-args: ("-nois") -*- *)
 (* 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) *)
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index a327bbf2a9..bb6af6a66c 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
+(* -*- coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *)
 (* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v
index c19a2d4a06..66dee702aa 100644
--- a/test-suite/bugs/closed/3956.v
+++ b/test-suite/bugs/closed/3956.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter"); mode: visual-line -*- *)
 Set Universe Polymorphism.
 Set Primitive Projections.
 Close Scope nat_scope.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index e4d76732a3..fc1c504f14 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,6 +1,6 @@
 Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
 (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1b..a8bf950ff2 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -1,5 +1,5 @@
 Unset Strict Universe Declaration.
-(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* -*- coq-prog-args: ("-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
 (* 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) *)
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
index 60c9354597..1ad81345db 100644
--- a/test-suite/bugs/closed/4394.v
+++ b/test-suite/bugs/closed/4394.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 
 Require Import Equality List.
 Inductive Foo (I : Type -> Type) (A : Type) : Type :=
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
index 5c23f8404b..a89cf0cbc3 100644
--- a/test-suite/bugs/closed/4400.v
+++ b/test-suite/bugs/closed/4400.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
 Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
 Set Printing Universes.
 Inductive Foo (I : Type -> Type) (A : Type) : Type :=
diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v
index a32acf789c..56a7b4f6e9 100644
--- a/test-suite/bugs/closed/4456.v
+++ b/test-suite/bugs/closed/4456.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *)
 (* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0
    coqtop version 8.5beta3 (November 2015) *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f0..4fab9d44f3 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-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 *)
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145d..ccef1c3040 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 1125 lines to 
 346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, 
 then from 285 lines to 271 lines *)
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c9318..82f1e3fe73 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *)
 (* 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) *)
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
index c89a86d634..a59eed2c86 100644
--- a/test-suite/bugs/closed/4656.v
+++ b/test-suite/bugs/closed/4656.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 Goal True.
   constructor 1.
 Qed.
diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v
index 1ae5081851..10e48db6dd 100644
--- a/test-suite/bugs/closed/4673.v
+++ b/test-suite/bugs/closed/4673.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3
    coqtop version 8.5 (February 2016) *)
 Axiom proof_admitted : False.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
index f047624c84..2d41828f19 100644
--- a/test-suite/bugs/closed/4722.v
+++ b/test-suite/bugs/closed/4722.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *)
+(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
index 3854bbffdd..cfb4548d2c 100644
--- a/test-suite/bugs/closed/4727.v
+++ b/test-suite/bugs/closed/4727.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
     (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
     o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
index a6ebda61cf..a90abd71cf 100644
--- a/test-suite/bugs/closed/4733.v
+++ b/test-suite/bugs/closed/4733.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
 Require Import Coq.Lists.List.
 Require Import Coq.Vectors.Vector.
diff --git a/test-suite/bugs/closed/4769.v b/test-suite/bugs/closed/4769.v
index d87906f313..33a1d1a50b 100644
--- a/test-suite/bugs/closed/4769.v
+++ b/test-suite/bugs/closed/4769.v
@@ -1,5 +1,5 @@
 
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "." "Top" "-top" "bug_hom_anom_10") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 156 lines to 41 lines, then from 237 lines to 45 lines, then from 163 lines to 66 lines, then from 342 lines to 121 lines, then from 353 lines to 184 lines, then from 343 lines to 255 lines, then from 435 lines to 322 lines, then from 475 lines to 351 lines, then from 442 lines to 377 lines, then from 505 lines to 410 lines, then from 591 lines to 481 lines, then from 596 lines to 535 lines, then from 647 lines to 570 lines, then from 669 lines to 596 lines, then from 687 lines to 620 lines, then from 728 lines to 652 lines, then from 1384 lines to 683 lines, then from 984 lines to 707 lines, then from 1124 lines to 734 lines, then from 775 lines to 738 lines, then from 950 lines to 763 lines, then from 857 lines to 798 lines, then from 983 lines to 752 lines, then from 1598 lines to 859 lines, then from 873 lines to 859 lines, then from 875 lines to 862 lines, then from 901 lines to 863 lines, then from 1047 lines to 865 lines, then from 929 lines to 871 lines, then from 989 lines to 884 lines, then from 900 lines to 884 lines, then from 884 lines to 751 lines, then from 763 lines to 593 lines, then from 482 lines to 232 lines, then from 416 lines to 227 lines, then from 290 lines to 231 lines, then from 348 lines to 235 lines, then from 249 lines to 235 lines, then from 249 lines to 172 lines, then from 186 lines to 172 lines, then from 140 lines to 113 lines, then from 127 lines to 113 lines *) (* coqc version trunk (June 2016) compiled on Jun 2 2016 10:16:20 with OCaml 4.02.3
    coqtop version trunk (June 2016) *)
 
diff --git a/test-suite/bugs/closed/4780.v b/test-suite/bugs/closed/4780.v
index 4cec43184c..71a51c6312 100644
--- a/test-suite/bugs/closed/4780.v
+++ b/test-suite/bugs/closed/4780.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Top" "-top" "bug_bad_induction_01") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-R" "." "Top" "-top" "bug_bad_induction_01") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 1889 lines to 144 lines, then from 158 lines to 144 lines *)
 (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3
    coqtop version 8.5pl1 (April 2016) *)
diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
index 9d65840acd..bbb34f465c 100644
--- a/test-suite/bugs/closed/4785_compat_85.v
+++ b/test-suite/bugs/closed/4785_compat_85.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.5") -*- *)
 Require Coq.Lists.List Coq.Vectors.Vector.
 Require Coq.Compat.Coq85.
 
diff --git a/test-suite/bugs/closed/4811.v b/test-suite/bugs/closed/4811.v
index a914962629..fe6e65a0f0 100644
--- a/test-suite/bugs/closed/4811.v
+++ b/test-suite/bugs/closed/4811.v
@@ -2,7 +2,7 @@
 
 (* Submitted by Jason Gross *)
 
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *)
 (* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3
    coqtop version 8.5pl1 (April 2016) *)
diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v
index 904abb2287..e411ce62f0 100644
--- a/test-suite/bugs/closed/4818.v
+++ b/test-suite/bugs/closed/4818.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-R" "." "Prob" "-top" "Product") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *)
 (* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3
    coqtop version 8.5pl1 (June 2016) *)
diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
index 7254afb429..72722f5f6d 100644
--- a/test-suite/bugs/closed/5198.v
+++ b/test-suite/bugs/closed/5198.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 286 lines to 
 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, 
 then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from 
diff --git a/test-suite/bugs/closed/HoTT_coq_012.v b/test-suite/bugs/closed/HoTT_coq_012.v
index a3c697f8ca..420aaf9745 100644
--- a/test-suite/bugs/closed/HoTT_coq_012.v
+++ b/test-suite/bugs/closed/HoTT_coq_012.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 
 Definition UU := Type.
 Inductive toto (B : UU) : UU := c (x : B).
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
index 3f5d7b0215..39a7103d1b 100644
--- a/test-suite/bugs/closed/HoTT_coq_032.v
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
 Set Implicit Arguments.
 Generalizable All Variables.
 Set Asymmetric Patterns.
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index e2bf1dbedb..263dec4857 100644
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Set Printing Universes.
 Set Implicit Arguments.
 Generalizable All Variables.
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index c687965937..635024e983 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
 Inductive Empty : Prop := .
 
 Inductive paths {A : Type} (a : A) : A -> Type :=
diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v
index a250987714..561b7e557d 100644
--- a/test-suite/bugs/closed/HoTT_coq_055.v
+++ b/test-suite/bugs/closed/HoTT_coq_055.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Set Universe Polymorphism.
 
 Inductive Empty : Prop := .
diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v
index 9c7e394dc3..2e6c735cf5 100644
--- a/test-suite/bugs/closed/HoTT_coq_059.v
+++ b/test-suite/bugs/closed/HoTT_coq_059.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Set Universe Polymorphism.
 
 Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x.
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index 90d1d18306..e01f73f1b3 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,6 +1,6 @@
 Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
 Set Universe Polymorphism.
 Definition admit {T} : T.
diff --git a/test-suite/bugs/closed/HoTT_coq_097.v b/test-suite/bugs/closed/HoTT_coq_097.v
index 38e8007b6c..f2b2e57b9c 100644
--- a/test-suite/bugs/closed/HoTT_coq_097.v
+++ b/test-suite/bugs/closed/HoTT_coq_097.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 Set Universe Polymorphism.
 Set Printing Universes.
 Inductive Empty : Set := .
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
index 7c1ab8dc2c..fa4072a8f6 100644
--- a/test-suite/bugs/closed/HoTT_coq_107.v
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *)
 (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
 (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
 Require Import Coq.Init.Logic.
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index b6c0da76ba..ea4bcd8b45 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
 (* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *)
 (* File reduced by coq-bug-finder from 139 lines to 124 lines. *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index 6ee6e65323..cd9cad4064 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *)
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") *)
 (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *)
 Set Universe Polymorphism.
 Set Asymmetric Patterns.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
index 4530548b8f..4541f13d01 100644
--- a/test-suite/bugs/opened/4803.v
+++ b/test-suite/bugs/opened/4803.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 (*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
 Require Import Coq.Lists.List.
 Require Import Coq.Vectors.Vector.
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
index 6611db70e2..1e9e919797 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-cutoff" "0.0") -*- *)
+(* -*- coq-prog-args: ("-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.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index 50131470eb..3dad6271af 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-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).
 
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index e69e23276b..b2e3c3e923 100644
--- a/test-suite/output/ErrorInModule.v
+++ b/test-suite/output/ErrorInModule.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
 Module M.
   Definition foo := nonexistent.
 End M.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
index 3036f8f05b..505c5ce378 100644
--- a/test-suite/output/ErrorInSection.v
+++ b/test-suite/output/ErrorInSection.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
 Section S.
   Definition foo := nonexistent.
 End S.
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
index db6348fa17..732a024fc1 100644
--- a/test-suite/success/Compat84.v
+++ b/test-suite/success/Compat84.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 
 Goal True.
   solve [ constructor 1 ]. Undo.
-- 
cgit v1.2.3


From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 09:04:17 +0200
Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5.

- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
---
 test-suite/success/Scheme.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index dd5aa81d1d..855f26698c 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -2,3 +2,26 @@
 
 Scheme Induction for eq Sort Prop.
 Check eq_ind_dep.
+
+(* This was broken in v8.5 *)
+
+Set Rewriting Schemes.
+Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a.
+Unset Rewriting Schemes.
+
+Check myeq_rect.
+Check myeq_ind.
+Check myeq_rec.
+Check myeq_congr.
+Check myeq_sym_internal.
+Check myeq_rew.
+Check myeq_rew_dep.
+Check myeq_rew_fwd_dep.
+Check myeq_rew_r.
+Check internal_myeq_sym_involutive.
+Check myeq_rew_r_dep.
+Check myeq_rew_fwd_r_dep.
+
+Set Rewriting Schemes.
+Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
+Unset Rewriting Schemes.
-- 
cgit v1.2.3


From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 test-suite/success/polymorphism.v | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd92..0a58fe89a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
 Type)) eq_refl.
 
-End Hurkens'.
\ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+  Set Universe Polymorphism.
+
+  Definition defaultid := (fun x => x) : Type -> Type.
+  Definition collapseid := defaultid@{_ _}.
+  Check collapseid@{_}.
+
+  Definition anonid := (fun x => x) : Type -> Type@{_}.
+  Check anonid@{_}.
+
+  Definition defaultalg := Type : Type.
+  Definition usedefaultalg := defaultalg@{_ _}.
+  Check usedefaultalg@{_ _}.
+
+  Definition anonalg := (fun x => x) (Type : Type@{_}).
+  Check anonalg@{_}.
+
+  Definition unrelated@{i j} := nat.
+  Definition useunrelated := unrelated@{_ _}.
+  Check useunrelated@{_ _}.
+
+  Definition inthemiddle@{i j k} :=
+    let _ := defaultid@{i j} in
+    defaultalg@{k j}.
+  (* i <= j < k *)
+  Definition collapsethemiddle := inthemiddle@{i _ j}.
+  Check collapsethemiddle@{_ _}.
+
+End Anonymous.
-- 
cgit v1.2.3


From 4361c1ed9ac5646055f9f0eecc4a003d720c1994 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 13:29:16 +0200
Subject: Type@{_} should not produce a flexible algebraic universe.

Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
---
 test-suite/success/polymorphism.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 0a58fe89a1..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -333,12 +333,12 @@ Module Anonymous.
   Definition anonid := (fun x => x) : Type -> Type@{_}.
   Check anonid@{_}.
 
-  Definition defaultalg := Type : Type.
-  Definition usedefaultalg := defaultalg@{_ _}.
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
   Check usedefaultalg@{_ _}.
 
-  Definition anonalg := (fun x => x) (Type : Type@{_}).
-  Check anonalg@{_}.
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
 
   Definition unrelated@{i j} := nat.
   Definition useunrelated := unrelated@{_ _}.
@@ -346,7 +346,7 @@ Module Anonymous.
 
   Definition inthemiddle@{i j k} :=
     let _ := defaultid@{i j} in
-    defaultalg@{k j}.
+    anonalg@{k j}.
   (* i <= j < k *)
   Definition collapsethemiddle := inthemiddle@{i _ j}.
   Check collapsethemiddle@{_ _}.
-- 
cgit v1.2.3


From 9b54bda96f51cc5387f195614620fae53dec5bd1 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 3 May 2017 10:47:53 +0200
Subject: FIx bug #5300: uncaught exception in "Print Assumptions".

---
 test-suite/bugs/closed/5300.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test-suite/bugs/closed/5300.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5300.v b/test-suite/bugs/closed/5300.v
new file mode 100644
index 0000000000..18202df508
--- /dev/null
+++ b/test-suite/bugs/closed/5300.v
@@ -0,0 +1,39 @@
+Module Test1.
+
+  Module Type Foo.
+    Parameter t : unit.
+  End Foo.
+
+  Module Bar : Foo.
+    Module Type Rnd. Definition t' : unit := tt. End Rnd.
+    Module Rnd_inst : Rnd. Definition t' : unit := tt. End Rnd_inst.
+    Definition t : unit.
+      exact Rnd_inst.t'.
+    Qed.
+  End Bar.
+
+  Print Assumptions Bar.t.
+End Test1.
+
+Module Test2.
+  Module Type Foo.
+    Parameter t1 : unit.
+    Parameter t2 : unit.
+  End Foo.
+
+  Module Bar : Foo.
+    Inductive ind := .
+    Definition t' : unit := tt.
+    Definition t1 : unit.
+    Proof.
+      exact ((fun (_ : ind -> False) => tt) (fun H => match H with end)).
+    Qed.
+    Definition t2 : unit.
+    Proof.
+      exact t'.
+    Qed.
+  End Bar.
+
+  Print Assumptions Bar.t1.
+  Print Assumptions Bar.t1.
+End Test2.
-- 
cgit v1.2.3


From cff6f53cbef53ce3902e59853f7a7dc9b7150f45 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 13:25:10 +0200
Subject: Adding a test-suite pattern-unification example that Econstr fixed.

---
 test-suite/success/unification.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 296686e16e..6f7498d659 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -188,3 +188,14 @@ Proof.
   apply idpath.
   apply idpath.
 Defined.
+
+(* An example where it is necessary to evar-normalize the instance of
+   an evar to evaluate if it is a pattern *)
+
+Check
+  let a := ?[P] in
+  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
+      x (p:x=0) =>
+    H ?[y] a p : x = 0.
+(* We have to solve "?P ?y[x] == x = 0" knowing from
+   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)
-- 
cgit v1.2.3


From 5e690404233e6c772c1d5ddc52142edf474953ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 May 2017 21:47:12 +0200
Subject: Cleaning old untested not any more interesting testing files.

---
 test-suite/bench/lists-100.v   | 107 ----------------------------
 test-suite/bench/lists_100.v   | 107 ----------------------------
 test-suite/kernel/inds.mv      |   3 -
 test-suite/misc/berardi_test.v | 153 -----------------------------------------
 4 files changed, 370 deletions(-)
 delete mode 100644 test-suite/bench/lists-100.v
 delete mode 100644 test-suite/bench/lists_100.v
 delete mode 100644 test-suite/kernel/inds.mv
 delete mode 100644 test-suite/misc/berardi_test.v

(limited to 'test-suite')

diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
deleted file mode 100644
index 5c64716c72..0000000000
--- a/test-suite/bench/lists-100.v
+++ /dev/null
@@ -1,107 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
-Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
-Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
-Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3.
-Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4.
-Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5.
-Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6.
-Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7.
-Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8.
-Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9.
-Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10.
-Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11.
-Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12.
-Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13.
-Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14.
-Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15.
-Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16.
-Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17.
-Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18.
-Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19.
-Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20.
-Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21.
-Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22.
-Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23.
-Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24.
-Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25.
-Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26.
-Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27.
-Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28.
-Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29.
-Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30.
-Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31.
-Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32.
-Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33.
-Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34.
-Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35.
-Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36.
-Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37.
-Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38.
-Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39.
-Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40.
-Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41.
-Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42.
-Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43.
-Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44.
-Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45.
-Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46.
-Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47.
-Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48.
-Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49.
-Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50.
-Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51.
-Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52.
-Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53.
-Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54.
-Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55.
-Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56.
-Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57.
-Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58.
-Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59.
-Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60.
-Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61.
-Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62.
-Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63.
-Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64.
-Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65.
-Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66.
-Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67.
-Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68.
-Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69.
-Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70.
-Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71.
-Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72.
-Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73.
-Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74.
-Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75.
-Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76.
-Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77.
-Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78.
-Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79.
-Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80.
-Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81.
-Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82.
-Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83.
-Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84.
-Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85.
-Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86.
-Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87.
-Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88.
-Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89.
-Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90.
-Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91.
-Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92.
-Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93.
-Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94.
-Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95.
-Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96.
-Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97.
-Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98.
-Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
deleted file mode 100644
index 5c64716c72..0000000000
--- a/test-suite/bench/lists_100.v
+++ /dev/null
@@ -1,107 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
-Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
-Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
-Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3.
-Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4.
-Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5.
-Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6.
-Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7.
-Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8.
-Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9.
-Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10.
-Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11.
-Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12.
-Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13.
-Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14.
-Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15.
-Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16.
-Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17.
-Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18.
-Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19.
-Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20.
-Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21.
-Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22.
-Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23.
-Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24.
-Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25.
-Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26.
-Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27.
-Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28.
-Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29.
-Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30.
-Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31.
-Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32.
-Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33.
-Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34.
-Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35.
-Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36.
-Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37.
-Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38.
-Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39.
-Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40.
-Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41.
-Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42.
-Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43.
-Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44.
-Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45.
-Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46.
-Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47.
-Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48.
-Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49.
-Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50.
-Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51.
-Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52.
-Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53.
-Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54.
-Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55.
-Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56.
-Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57.
-Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58.
-Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59.
-Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60.
-Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61.
-Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62.
-Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63.
-Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64.
-Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65.
-Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66.
-Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67.
-Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68.
-Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69.
-Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70.
-Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71.
-Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72.
-Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73.
-Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74.
-Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75.
-Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76.
-Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77.
-Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78.
-Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79.
-Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80.
-Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81.
-Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82.
-Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83.
-Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84.
-Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85.
-Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86.
-Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87.
-Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88.
-Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89.
-Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90.
-Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91.
-Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92.
-Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93.
-Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94.
-Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95.
-Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96.
-Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97.
-Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98.
-Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99.
diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv
deleted file mode 100644
index bd1cc49f86..0000000000
--- a/test-suite/kernel/inds.mv
+++ /dev/null
@@ -1,3 +0,0 @@
-Inductive [] nat : Set := O : nat | S : nat->nat.
-Check Construct nat 0 1.
-Check Construct nat 0 2.
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
deleted file mode 100644
index a64db4dab7..0000000000
--- a/test-suite/misc/berardi_test.v
+++ /dev/null
@@ -1,153 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file formalizes Berardi's paradox which says that in
-   the calculus of constructions, excluded middle (EM) and axiom of
-   choice (AC) imply proof irrelevance (PI).
-   Here, the axiom of choice is not necessary because of the use
-   of inductive types.
-<<
-@article{Barbanera-Berardi:JFP96,
-   author    = {F. Barbanera and S. Berardi},
-   title     = {Proof-irrelevance out of Excluded-middle and Choice
-                in the Calculus of Constructions},
-   journal   = {Journal of Functional Programming},
-   year      = {1996},
-   volume    = {6},
-   number    = {3},
-   pages     = {519-525}
-}
->> *)
-
-Set Implicit Arguments.
-
-Section Berardis_paradox.
-
-(** Excluded middle *)
-Hypothesis EM : forall P:Prop, P \/ ~ P.
-
-(** Conditional on any proposition. *)
-Definition IFProp (P B:Prop) (e1 e2:P) :=
-  match EM B with
-  | or_introl _ => e1
-  | or_intror _ => e2
-  end.
-
-(** Axiom of choice applied to disjunction.
-    Provable in Coq because of dependent elimination. *)
-Lemma AC_IF :
- forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
-   (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
-Proof.
-intros P B e1 e2 Q p1 p2.
-unfold IFProp.
-case (EM B); assumption.
-Qed.
-
-
-(** We assume a type with two elements. They play the role of booleans.
-    The main theorem under the current assumptions is that [T=F] *)
-Variable Bool : Prop.
-Variable T : Bool.
-Variable F : Bool.
-
-(** The powerset operator *)
-Definition pow (P:Prop) := P -> Bool.
-
-
-(** A piece of theory about retracts *)
-Section Retracts.
-
-Variables A B : Prop.
-
-Record retract : Prop :=
-  {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
-
-Record retract_cond : Prop :=
-  {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
-
-
-(** The dependent elimination above implies the axiom of choice: *)
-Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
-Proof.
-intros r.
-case r; simpl.
-trivial.
-Qed.
-
-End Retracts.
-
-(** This lemma is basically a commutation of implication and existential
-    quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
-    which is provable in classical logic ( => is already provable in
-    intuitionnistic logic). *)
-
-Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
-Proof.
-intros A B.
-destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
-  exists f0 g0; trivial.
-  exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
-    destruct hf; auto.
-Qed.
-
-
-(** The paradoxical set *)
-Definition U := forall P:Prop, pow P.
-
-(** Bijection between [U] and [(pow U)] *)
-Definition f (u:U) : pow U := u U.
-
-Definition g (h:pow U) : U :=
-  fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).
-
-(** We deduce that the powerset of [U] is a retract of [U].
-    This lemma is stated in Berardi's article, but is not used
-    afterwards. *)
-Lemma retract_pow_U_U : retract (pow U) U.
-Proof.
-exists g f.
-intro a.
-unfold f, g; simpl.
-apply AC.
-exists (fun x:pow U => x) (fun x:pow U => x).
-trivial.
-Qed.
-
-(** Encoding of Russel's paradox *)
-
-(** The boolean negation. *)
-Definition Not_b (b:Bool) := IFProp (b = T) F T.
-
-(** the set of elements not belonging to itself *)
-Definition R : U := g (fun u:U => Not_b (u U u)).
-
-
-Lemma not_has_fixpoint : R R = Not_b (R R).
-Proof.
-unfold R at 1.
-unfold g.
-rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
-trivial.
-exists (fun x:pow U => x) (fun x:pow U => x); trivial.
-Qed.
-
-
-Theorem classical_proof_irrelevence : T = F.
-Proof.
-generalize not_has_fixpoint.
-unfold Not_b.
-apply AC_IF.
-intros is_true is_false.
-elim is_true; elim is_false; trivial.
-
-intros not_true is_true.
-elim not_true; trivial.
-Qed.
-
-End Berardis_paradox.
-- 
cgit v1.2.3


From 7f17e151c0a2666263d3854c064acdfea29edf53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 May 2017 17:19:22 +0200
Subject: Adding tests for testing exit status and #use"include".

---
 test-suite/.csdp.cache                | Bin 89077 -> 89077 bytes
 test-suite/Makefile                   |  30 +++++++++++++++++++++++++++++-
 test-suite/misc/exitstatus/illtyped.v |   1 +
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/misc/exitstatus/illtyped.v

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd3..b99d80e95f 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c10cd4ed44..779f5455ae 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,6 +33,7 @@ LIB := $(shell cd ..; pwd)
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
 bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqtopbyte := $(BIN)coqtop.byte
 
 command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
 coqc := $(coqtop) -compile
@@ -405,7 +406,7 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log
+misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log
 
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
@@ -477,6 +478,33 @@ misc/universes.log: misc/universes/all_stdlib.v
 misc/universes/all_stdlib.v:
 	cd .. && $(MAKE) test-suite/$@
 
+misc/printers.log:
+	@echo "TEST      printers"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/printers...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/printers...Error!"; \
+	  fi; \
+	} > "$@"
+
+misc/exitstatus.log:
+	@echo "TEST      exitstatus"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/exitstatus...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/exitstatus...Error!"; \
+	  fi; \
+	} > "$@"
 
 # IDE : some tests of backtracking for coqtop -ideslave
 
diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v
new file mode 100644
index 0000000000..df6bbb389c
--- /dev/null
+++ b/test-suite/misc/exitstatus/illtyped.v
@@ -0,0 +1 @@
+Check S S.
-- 
cgit v1.2.3


From 63510329fae28f7a9d18935f24e3ebf0485dabc8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 May 2017 18:28:55 +0200
Subject: A more regular naming of variables in test-suite Makefile.

---
 test-suite/Makefile | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 779f5455ae..5d3c118445 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -31,12 +31,12 @@ BIN := ../bin/
 LIB := $(shell cd ..; pwd)
 
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
-bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
-bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 coqtopbyte := $(BIN)coqtop.byte
 
-command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
-coqc := $(coqtop) -compile
+coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
+coqtopcompile := $(coqtop) -compile
 coqdep := $(BIN)coqdep -coqlib $(LIB)
 
 SHOW := $(if $(VERBOSE),@true,@echo)
@@ -53,7 +53,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_
 # 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-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))
+get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload))
 
 
 bogomips:=
@@ -220,7 +220,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...could not be prepared" ; \
@@ -250,7 +250,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
+	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
 	    $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
@@ -421,8 +421,8 @@ misc/deps-order.log:
 	  $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
 	    | head -n 1 > $$tmpoutput; \
 	  diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \
-	  $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
-	  $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
+	  $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
+	  $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
 	  $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
 	  S=$$?; times; \
 	  if [ $$R = 0 -a $$S = 0 ]; then \
@@ -441,9 +441,9 @@ misc/deps-checksum.log:
 	$(HIDE){ \
 	  echo $(call log_intro,deps-checksum); \
 	  rm -f misc/deps/*/*.vo; \
-	  $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \
-	  $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \
-	  $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \
+	  $(coqc) -R misc/deps/A A misc/deps/A/A.v; \
+	  $(coqc) -R misc/deps/B A misc/deps/B/A.v; \
+	  $(coqc) -R misc/deps/B A misc/deps/B/B.v; \
 	  $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
@@ -461,8 +461,8 @@ universes: misc/universes.log
 misc/universes.log: misc/universes/all_stdlib.v
 	@echo "TEST      misc/universes"
 	$(HIDE){ \
-	  $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
-	  $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \
+	  $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
+	  $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \
 	  mv universes.txt misc/universes; \
 	  N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
 	  times; \
@@ -529,9 +529,9 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 %.vio.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(bincoqc) -quick -R vio vio $* 2>&1 && \
+	  $(coqc) -quick -R vio vio $* 2>&1 && \
 	  $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
-	  $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
+	  $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -546,8 +546,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 %.chk.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(bincoqc) -R coqchk coqchk $* 2>&1 && \
-	  $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \
+	  $(coqc) -R coqchk coqchk $* 2>&1 && \
+	  $(coqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
-- 
cgit v1.2.3


From 98a927aefb6df05a957d94cf2fd22d88e9e6c6b6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 May 2017 21:48:43 +0200
Subject: Moving code for miscellaneous tests to specific files.

The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.

This avoids making the main Makefile more or more complex.

We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.

Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
---
 test-suite/Makefile              | 102 +++++----------------------------------
 test-suite/misc/deps-checksum.sh |   5 ++
 test-suite/misc/deps-order.sh    |  20 ++++++++
 test-suite/misc/exitstatus.sh    |   7 +++
 test-suite/misc/printers.sh      |   3 ++
 test-suite/misc/universes.sh     |   8 +++
 6 files changed, 54 insertions(+), 91 deletions(-)
 create mode 100755 test-suite/misc/deps-checksum.sh
 create mode 100755 test-suite/misc/deps-order.sh
 create mode 100755 test-suite/misc/exitstatus.sh
 create mode 100755 test-suite/misc/printers.sh
 create mode 100755 test-suite/misc/universes.sh

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5d3c118445..39ef05269f 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -406,103 +406,23 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log
-
-# Check that both coqdep and coqtop/coqc supports -R
-# Check that both coqdep and coqtop/coqc takes the later -R
-# See bugs 2242, 2337, 2339
-deps-order: misc/deps-order.log
-misc/deps-order.log:
-	@echo "TEST      misc/deps-order"
-	$(HIDE){ \
-	  echo $(call log_intro,deps-order); \
-	  rm -f misc/deps/*/*.vo; \
-	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
-	  $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
-	    | head -n 1 > $$tmpoutput; \
-	  diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \
-	  $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
-	  $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
-	  $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
-	  S=$$?; times; \
-	  if [ $$R = 0 -a $$S = 0 ]; then \
-	    echo $(log_success); \
-	    echo "    misc/deps-order...Ok"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/deps-order...Error! (unexpected order)"; \
-	  fi; \
-	  rm $$tmpoutput; \
-	} > "$@"
-
-deps-checksum: misc/deps-checksum.log
-misc/deps-checksum.log:
-	@echo "TEST      misc/deps-checksum"
-	$(HIDE){ \
-	  echo $(call log_intro,deps-checksum); \
-	  rm -f misc/deps/*/*.vo; \
-	  $(coqc) -R misc/deps/A A misc/deps/A/A.v; \
-	  $(coqc) -R misc/deps/B A misc/deps/B/A.v; \
-	  $(coqc) -R misc/deps/B A misc/deps/B/B.v; \
-	  $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
-	  if [ $$? = 0 ]; then \
-	    echo $(log_success); \
-	    echo "    misc/deps-checksum...Ok"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/deps-checksum...Error!"; \
-	  fi; \
-	} > "$@"
-
+misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
 
-# Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 4 # Prop is not counted
-universes: misc/universes.log
-misc/universes.log: misc/universes/all_stdlib.v
-	@echo "TEST      misc/universes"
-	$(HIDE){ \
-	  $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
-	  $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \
-	  mv universes.txt misc/universes; \
-	  N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
-	  times; \
-	  if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \
-	    echo $(log_success); \
-	    echo "    misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \
-	  fi; \
-	} > "$@"
-
-misc/universes/all_stdlib.v:
-	cd .. && $(MAKE) test-suite/$@
-
-misc/printers.log:
-	@echo "TEST      printers"
-	$(HIDE){ \
-	  echo $(call log_intro,$<); \
-	  printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \
-	  if [ $$R != 0 ]; then \
-	    echo $(log_success); \
-	    echo "    misc/printers...Ok"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/printers...Error!"; \
-	  fi; \
-	} > "$@"
-
-misc/exitstatus.log:
-	@echo "TEST      exitstatus"
+$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
+	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \
-	  if [ $$R != 0 ]; then \
+	  export coqc="$(coqc)"; \
+	  export coqtop="$(coqtop)"; \
+	  export coqdep="$(coqdep)"; \
+	  export coqtopbyte="$(coqtopbyte)"; \
+	  "$<" 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-	    echo "    misc/exitstatus...Ok"; \
+	    echo "    $<...Ok"; \
 	  else \
 	    echo $(log_failure); \
-	    echo "    misc/exitstatus...Error!"; \
+	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
 
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
new file mode 100755
index 0000000000..1e2afb7540
--- /dev/null
+++ b/test-suite/misc/deps-checksum.sh
@@ -0,0 +1,5 @@
+rm -f misc/deps/*/*.vo
+$coqc -R misc/deps/A A misc/deps/A/A.v
+$coqc -R misc/deps/B A misc/deps/B/A.v
+$coqc -R misc/deps/B A misc/deps/B/B.v
+$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
new file mode 100755
index 0000000000..375b706f0a
--- /dev/null
+++ b/test-suite/misc/deps-order.sh
@@ -0,0 +1,20 @@
+# Check that both coqdep and coqtop/coqc supports -R
+# Check that both coqdep and coqtop/coqc takes the later -R
+# See bugs 2242, 2337, 2339
+rm -f misc/deps/*/*.vo
+tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
+diff -u misc/deps/deps.out $tmpoutput 2>&1
+R=$?
+times
+$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
+$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
+$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1
+S=$?
+if [ $R = 0 -a $S = 0 ]; then
+    printf "coqdep and coqtop agree\n"
+    exit 0
+else
+    printf "coqdep and coqtop disagree\n"
+    exit 1
+fi
diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh
new file mode 100755
index 0000000000..cea1de862f
--- /dev/null
+++ b/test-suite/misc/exitstatus.sh
@@ -0,0 +1,7 @@
+$coqtop -load-vernac-source misc/exitstatus/illtyped.v
+N=$?
+$coqc misc/exitstatus/illtyped.v
+P=$?
+printf "On ill-typed input, coqtop returned $N.\n"
+printf "On ill-typed input, coqc returned $P.\n"
+if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi
diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
new file mode 100755
index 0000000000..c822d0eb37
--- /dev/null
+++ b/test-suite/misc/printers.sh
@@ -0,0 +1,3 @@
+printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound
+if [ $? = 0 ]; then exit 1; else exit 0; fi
+
diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh
new file mode 100755
index 0000000000..d87a86035c
--- /dev/null
+++ b/test-suite/misc/universes.sh
@@ -0,0 +1,8 @@
+# Sort universes for the whole standard library
+EXPECTED_UNIVERSES=4 # Prop is not counted
+$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1
+$coqc -R misc/universes Universes misc/universes/universes 2>&1
+mv universes.txt misc/universes
+N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l`
+printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES
+if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi
-- 
cgit v1.2.3


From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:10:57 +0200
Subject: Fixing a bug with nested "as" clauses in "match".

---
 test-suite/success/Cases.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 49c465b6c6..52fe98ac07 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
 Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
 
 Check match niln in listn O return O=O with niln => eq_refl end.
+
+(* A test about nested "as" clauses *)
+(* (was failing up to May 2017) *)
+
+Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
-- 
cgit v1.2.3


From 00964706efe8f6b13e38b57ddb45fac516feb958 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 May 2017 23:31:08 +0200
Subject: Fixing bug #5222 (anomaly with "`pat" in the presence of scope
 delimiters).

We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.

More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
---
 test-suite/bugs/closed/5522.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5522.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v
new file mode 100644
index 0000000000..0fae9ede42
--- /dev/null
+++ b/test-suite/bugs/closed/5522.v
@@ -0,0 +1,7 @@
+(* Checking support for scope delimiters and as clauses in 'pat
+   applied to notations with binders *)
+
+Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. )
+  (at level 200, x binder, y binder, f at level 200).
+
+Check multifun '((x, y)%core as z) in (x+y,0)=z.
-- 
cgit v1.2.3


From 697cd5a8e7927873ed6700c7e906ae3675bd98b1 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 May 2017 10:30:50 +0200
Subject: Simplified compaction criterion + tests.

---
 test-suite/output/CompactContexts.out | 7 +++++++
 test-suite/output/CompactContexts.v   | 5 +++++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/output/CompactContexts.out
 create mode 100644 test-suite/output/CompactContexts.v

(limited to 'test-suite')

diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out
new file mode 100644
index 0000000000..9d1d19877e
--- /dev/null
+++ b/test-suite/output/CompactContexts.out
@@ -0,0 +1,7 @@
+1 subgoal
+  
+  hP1 : True
+  a : nat   b : list nat   h : forall x : nat, {y : nat | y > x}
+  h2 : True
+  ============================
+  False
diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v
new file mode 100644
index 0000000000..07588d34f9
--- /dev/null
+++ b/test-suite/output/CompactContexts.v
@@ -0,0 +1,5 @@
+Set Printing Compact Contexts.
+
+Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False.
+Show.
+Abort.
\ No newline at end of file
-- 
cgit v1.2.3


From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:31:08 +0200
Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick
 to EXTEND.

---
 test-suite/success/ltac.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..9ab47fedea 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,9 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* Test evar syntax *)
+
+Goal True.
+evar (0=0).
+Abort.
-- 
cgit v1.2.3