From 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 8 Sep 2016 14:19:02 +0200
Subject: Fix Bug #5073 : regression of micromega plugin

The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
---
 test-suite/micromega/zomicron.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 3f4c2407d2..239bc69360 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -82,4 +82,11 @@ Proof.
   lia.
 Qed.
 
+(*  Bug 5073 *)
+Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+Proof.
+  lia.
+Qed.
+
+
 
-- 
cgit v1.2.3


From e65c629bac48e61b3a14f05bfafc6b85486359c0 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Thu, 8 Sep 2016 23:23:36 +0200
Subject: Fix Bug #5073 : regression of micromega plugin

esprit d'escalier : is now also fixed for R
---
 test-suite/micromega/rexample.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 12f72a5809..bd52270100 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -81,3 +81,8 @@ Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; lra.
 Qed.
 
+(*  Bug 5073 *)
+Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+Proof.
+  lra.
+Qed.
-- 
cgit v1.2.3


From 01d0c1224e0a29f10b2cef5b3fd2b4d06a686055 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Sep 2016 11:30:41 +0200
Subject: Update csdp cache.

This was making the test-suite fail on machines where csdp was not installed.
---
 test-suite/.csdp.cache | Bin 79491 -> 89077 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index 75dd38fde8..b8c07512f3 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
-- 
cgit v1.2.3


From a9efa6f9e601cc2bfa1968dca1cdc0d01ebf55e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Sep 2016 17:09:59 +0200
Subject: Fix output test-suite after commit 0d3c319.

---
 test-suite/output/Errors.out |  2 +-
 test-suite/output/ltac.out   | 17 +++++++++++------
 2 files changed, 12 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 62e9ef4b20..06a6b2d157 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -6,5 +6,5 @@ The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
-Ltac call to "instantiate" failed.
+Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21554e9ff8..f4254e4e2f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -4,20 +4,25 @@ Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z
 The command has indeed failed with message:
-In nested Ltac calls to "g1" and "refine", last call failed.
+In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f1" and "refine", last call failed.
+In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.
-- 
cgit v1.2.3


From 43869b4e05824244e666c60e0b740a80e8b09d0c Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 28 Jun 2016 12:37:00 -0400
Subject: no-refold patch

Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
---
 test-suite/bugs/closed/3424.v | 1 +
 test-suite/output/inference.v | 1 +
 2 files changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v
index f9b2c38611..ee8cabf171 100644
--- a/test-suite/bugs/closed/3424.v
+++ b/test-suite/bugs/closed/3424.v
@@ -13,6 +13,7 @@ Notation "0" := (trunc_S minus_one) : trunc_scope.
 Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
 Notation IsHProp := (IsTrunc minus_one).
 Notation IsHSet := (IsTrunc 0).
+Set Refolding Reduction.
 Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }.
 Proof.
 intros.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12b2..1825db1676 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 
 
-- 
cgit v1.2.3


From 74f8381ed943f1e786b32c49fb31f14fd488dc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 10 Sep 2016 11:37:21 +0200
Subject: Test for #5077.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v
new file mode 100644
index 0000000000..7e7f2c3737
--- /dev/null
+++ b/test-suite/bugs/closed/5077.v
@@ -0,0 +1,8 @@
+(* Testing robustness of typing for a fixpoint with evars in its type *)
+
+Inductive foo (n : nat) : Type := .
+Definition foo_denote {n} (x : foo n) : Type := match x with end.
+
+Definition baz : forall n (x : foo n), foo_denote x.
+refine (fix go n (x : foo n) : foo_denote x := _).
+Abort.  
-- 
cgit v1.2.3


From 650550fc95d5ba41da84e2003371522221e27734 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 18 Jun 2016 19:07:42 -0400
Subject: Add a test for 4836

This required improving the machinery of the test-suite Makefile to
support -compile.
---
 test-suite/Makefile                         | 18 ++++++++++--------
 test-suite/bugs/closed/PLACEHOLDER.v        |  0
 test-suite/bugs/closed/bug_4836.v           |  1 +
 test-suite/bugs/closed/bug_4836/PLACEHOLDER |  0
 4 files changed, 11 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bugs/closed/PLACEHOLDER.v
 create mode 100644 test-suite/bugs/closed/bug_4836.v
 create mode 100644 test-suite/bugs/closed/bug_4836/PLACEHOLDER

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81321729d4..c918e92d6b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,6 +49,9 @@ SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
+# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
+has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
+get_command_based_on_flags = $(if $(call has_compile_flag,$(1)),$(coqc),$(command))
 
 
 bogomips:=
@@ -172,7 +175,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
 	@echo "TEST      $<  $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...still active"; \
@@ -193,7 +196,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -256,7 +259,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
@@ -311,7 +314,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+	  res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
@@ -341,7 +344,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	      echo $(log_success); \
 	      echo "    $<...still wished"; \
@@ -483,4 +486,3 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
-
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
new file mode 100644
index 0000000000..5838dcd8a7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
new file mode 100644
index 0000000000..e69de29bb2
-- 
cgit v1.2.3


From 12cedcbf4dcfe4fd43ab9f4b648314cac26b82db Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 3 Jul 2016 17:13:37 -0400
Subject: Add support for testing output mod timing changes

Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages.  (This can potentially be
extended later.)

Add a test-suite file to make sure that LtacProf outputs some table.
---
 test-suite/Makefile                        | 33 ++++++++++++++++++++++++++++--
 test-suite/output-modulo-time/ltacprof.out | 12 +++++++++++
 test-suite/output-modulo-time/ltacprof.v   |  8 ++++++++
 3 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/output-modulo-time/ltacprof.out
 create mode 100644 test-suite/output-modulo-time/ltacprof.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index c918e92d6b..a3050bfccc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,8 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-get_command_based_on_flags = $(if $(call has_compile_flag,$(1)),$(coqc),$(command))
+has_profile_ltac_or_compile_flag = $(filter "-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))
 
 
 bogomips:=
@@ -82,7 +83,7 @@ COMPLEXITY := $(if $(bogomips),complexity)
 BUGS := bugs/opened bugs/closed
 
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
-  interactive micromega $(COMPLEXITY) modules stm
+  output-modulo-time interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
@@ -136,6 +137,7 @@ summary:
 	  $(call summary_dir, "Failure tests", failure); \
 	  $(call summary_dir, "Bugs tests", bugs); \
 	  $(call summary_dir, "Output tests", output); \
+	  $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \
 	  $(call summary_dir, "Interactive tests", interactive); \
 	  $(call summary_dir, "Micromega tests", micromega); \
 	  $(call summary_dir, "Miscellaneous tests", misc); \
@@ -291,6 +293,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	  rm $$tmpoutput; \
 	} > "$@"
 
+$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
+	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+	    | grep -v "Welcome to Coq" \
+	    | grep -v "\[Loading ML file" \
+	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
+	    | sed 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	    | sed 's/\s*0\.\s*//g' \
+	    > $$tmpoutput; \
+	  sed 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \
+	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (unexpected output)"; \
+	  fi; \
+	  rm $$tmpoutput; \
+	  rm $$tmpexpected; \
+	} > "$@"
+
 $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out
new file mode 100644
index 0000000000..cc04c2c9bd
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.out
@@ -0,0 +1,12 @@
+total time:      1.528s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0%       1    1.528s
+─constructor ---------------------------   0.0%   0.0%       1    0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
new file mode 100644
index 0000000000..d79451f0f7
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+  idtac. idtac. sleep. constructor.
+Defined.
-- 
cgit v1.2.3


From 90e5945e1666540bc18e7a9b831d136041f4e487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Sep 2016 17:22:03 +0200
Subject: Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.

---
 test-suite/output/Notations2.out | 2 ++
 test-suite/output/Notations2.v   | 5 +++++
 2 files changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d38372..13ed7816d8 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,5 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7d..3f3945052e 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
-- 
cgit v1.2.3


From 881d38c4c64fb3f3c346d5fbea15999fd6110ae9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Sep 2016 12:55:00 +0200
Subject: test-suite/output-modulo-time made more robust

---
 test-suite/Makefile | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index a3050bfccc..1dfbb29ff0 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -304,10 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
-	    | sed 's/\s*[0-9]*\.[0-9]\+\s*//g' \
-	    | sed 's/\s*0\.\s*//g' \
+	    | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+	          -e 's/\s*0\.\s*//g' \
+		  -e 's/\s*[-+]nan\s*//g' \
+		  -e 's/\s*[-+]inf\s*//g' \
 	    > $$tmpoutput; \
-	  sed 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \
+	  sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+		-e 's/\s*0\.\s*//g' \
+		-e 's/\s*[-+]nan\s*//g' \
+		-e 's/\s*[-+]inf\s*//g' \
+       	       $*.out > $$tmpexpected; \
 	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-- 
cgit v1.2.3


From 2aaa58c22e37b05e3637ac7161bb464da7db054a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Sep 2016 10:22:41 +0200
Subject: Fixing test-suite after commit 43104a0b.

---
 test-suite/success/TestRefine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862fa..023cb5f59d 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3