5 files changed, 56 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f41fb5b1e4..32e245e362 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  output=$*.out.real; \
 	  $(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/File "[^"]*"/File "stdin"/' \
-	    > $$tmpoutput; \
-	  diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \
+	    > $$output; \
+	  diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
+	    rm $$output; \
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
 	    $(FAIL); \
 	  fi; \
-	  rm $$tmpoutput; \
 	} > "$@"
 
+.PHONY: approve-output
+approve-output: output
+	$(HIDE)for f in output/*.out.real; do \
+	  mv "$$f" "$${f%.real}"; \
+	  echo "Updated $${f%.real}!"; \
+	done
+
 # the expected output for the MExtraction test is
 # /plugins/micromega/micromega.ml except with additional newline
 output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/README.md b/test-suite/README.md
index 4572c98cfe..ef2e574ece 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file
 
 There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
 unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
+
+## Fixing output tests
+
+When an output test `output/foo.v` fails, the output is stored in
+`output/foo.out.real`. Move that file to the reference file
+`output/foo.out` to update the test, approving the new output. Target
+`approve-output` will do this for all failing output tests
+automatically.
+
+Don't forget to check the updated `.out` files into git!
+
+Note that `output/MExtraction.out` is special: it is copied from
+`micromega/micromega.ml` in the plugin source directory. Automatic
+approval will incorrectly update the copy.
diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v
new file mode 100644
index 0000000000..9fadb195bf
--- /dev/null
+++ b/test-suite/bugs/closed/7068.v
@@ -0,0 +1,6 @@
+(* These tests are only about a subset of #7068 *)
+(* The original issue is still open *)
+
+Inductive foo : let T := Type in T := .
+Definition bob1 := Eval vm_compute in foo_rect.
+Definition bob2 := Eval native_compute in foo_rect.
diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v
new file mode 100644
index 0000000000..0abc88c282
--- /dev/null
+++ b/test-suite/bugs/closed/7076.v
@@ -0,0 +1,4 @@
+(* These calls were raising an anomaly at some time *)
+Inductive A : nat -> id (nat->Type) := .
+Eval vm_compute in fun x => match x in A y z return y = z with end.
+Eval native_compute in fun x => match x in A y z return y = z with end.
diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v
new file mode 100644
index 0000000000..34eb8b8676
--- /dev/null
+++ b/test-suite/bugs/closed/7631.v
@@ -0,0 +1,21 @@
+Module NamedContext.
+
+Definition foo := true.
+
+Section Foo.
+
+Let bar := foo.
+
+Eval native_compute in bar.
+
+End Foo.
+
+End NamedContext.
+
+Module RelContext.
+
+Definition foo := true.
+
+Definition bar (x := foo) := Eval native_compute in x.
+
+End RelContext.