20 files changed, 277 insertions, 27 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b3a633e528..265c2eafa7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -530,14 +530,16 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \
+	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished .*transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be accepted)" ; \
+	    $(FAIL); \
 	  elif [ "$$res" = "" ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (couldn't find a time measure)"; \
+	    $(FAIL); \
 	  else \
 	    true "express effective time in centiseconds"; \
 	    resorig="$$res"; \
@@ -641,7 +643,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 %.vio.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(coqc) -quick -R vio vio $* 2>&1 && \
+	  $(coqc) -vio -R vio vio $* 2>&1 && \
 	  $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \
 	  $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v
new file mode 100644
index 0000000000..ca806ea324
--- /dev/null
+++ b/test-suite/bugs/bug_11140.v
@@ -0,0 +1,11 @@
+Axiom T : nat -> Prop.
+Axiom f : forall x, T x.
+Arguments f & x.
+
+Lemma test : (f (1 + _) : T 2) = f 2.
+match goal with
+| |- (f (1 + 1) = f 2) => idtac
+| |- (f 2 = f 2) => fail (* Issue 11140 *)
+| |- _ => fail
+end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v
new file mode 100644
index 0000000000..87f15a4a19
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11133.v
@@ -0,0 +1,18 @@
+Module Type Universe.
+Parameter U : nat.
+End Universe.
+
+Module Univ_prop (Univ : Universe).
+Include Univ.
+End Univ_prop.
+
+Module Monad (Univ : Universe).
+Module UP := (Univ_prop Univ).
+End Monad.
+
+Module Rules (Univ:Universe).
+Module MP := Monad Univ.
+Include MP.
+Import UP.
+Definition M := UP.U.    (* anomaly here *)
+End Rules.
diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v
new file mode 100644
index 0000000000..6e109e33e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11168.v
@@ -0,0 +1,5 @@
+Axiom f : forall T, T.
+Arguments f &.
+Check f _ _.
+Check f (_ -> _) _.
+Check f (forall x, _) _.
diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v
new file mode 100644
index 0000000000..d8bc4a9f02
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11360.v
@@ -0,0 +1,6 @@
+Section S.
+  Variable (A:Type).
+  #[universes(template)]
+  Inductive bar (d:A) := .
+End S.
+Check bar nat 0.
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh
index e1f17725dc..13e484b852 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/003-non-utf8/run.sh
@@ -5,20 +5,14 @@ set -e
 
 cd "$(dirname "${BASH_SOURCE[0]}")"
 
-python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log2 || exit $?
-python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log3 || exit $?
+"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log || exit $?
 
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $?
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $?
+diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $?
 
-cat time-of-build.log.in | python2 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log2 || exit $?
-cat time-of-build.log.in | python3 "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log3 || exit $?
+cat time-of-build.log.in | "$COQLIB"/tools/make-one-time-file.py - time-of-build-pretty.log || exit $?
 
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $?
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $?
+diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $?
 
-(python2 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log2
-(python3 "$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log3
+("$COQLIB"/tools/make-one-time-file.py time-of-build.log.in - || exit $?) > time-of-build-pretty.log
 
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log2 || exit $?
-diff -u time-of-build-pretty.log.expected time-of-build-pretty.log3 || exit $?
+diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $?
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
index 9f3b648aa3..cfacf738a3 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
@@ -9,3 +9,4 @@ export COQLIB
 
 ./001-correct-diff-sorting-order/run.sh
 ./002-single-file-sorting/run.sh
+./003-non-utf8/run.sh
diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out
new file mode 100644
index 0000000000..0b4b4b6e37
--- /dev/null
+++ b/test-suite/coqdoc/bug11353.html.out
@@ -0,0 +1,39 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.bug11353</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug11353</h1>
+
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[   <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/>
+<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
+&nbsp;&nbsp;| <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/>
+&nbsp;&nbsp;| <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/>
+
+<br/>
+#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
+\ No newline at end of file
diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out
new file mode 100644
index 0000000000..a6478682d8
--- /dev/null
+++ b/test-suite/coqdoc/bug11353.tex.out
@@ -0,0 +1,34 @@
+\documentclass[12pt]{report}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.bug11353}{Library }{Coqdoc.bug11353}
+
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[   \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol
+\coqdocnoindent
+\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug11353.v b/test-suite/coqdoc/bug11353.v
new file mode 100644
index 0000000000..b68902c8cc
--- /dev/null
+++ b/test-suite/coqdoc/bug11353.v
@@ -0,0 +1,7 @@
+(* -*- coq-prog-args: ("-g") -*- *)
+Definition a := 0. #[ (* templatize *)  universes( template) ]
+Inductive mysum (A B:Type) : Type :=
+  | myinl : A -> mysum A B
+  | myinr : B -> mysum A B.
+
+#[local]Definition b := 1.
diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v
new file mode 100644
index 0000000000..57c1d7d52f
--- /dev/null
+++ b/test-suite/micromega/bug_11191a.v
@@ -0,0 +1,6 @@
+Require Import ZArith Lia.
+
+Goal forall p n, (0 < Z.pos (p ^ n))%Z.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v
new file mode 100644
index 0000000000..007470c5b3
--- /dev/null
+++ b/test-suite/micromega/bug_11191b.v
@@ -0,0 +1,6 @@
+Require Import ZArith Lia.
+
+Goal forall p, (0 < Z.pos (p ^ 2))%Z.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh
index 96bdee2fc2..e60fb48bca 100755
--- a/test-suite/misc/quick-include.sh
+++ b/test-suite/misc/quick-include.sh
@@ -1,5 +1,5 @@
 #!/bin/sh
 set -e
 
-$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v
-$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v
+$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v
+$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index b2e3c3e923..fbb3c6bdab 100644
--- a/test-suite/output/ErrorInModule.v
+++ b/test-suite/output/ErrorInModule.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-vio") -*- *)
 Module M.
   Definition foo := nonexistent.
 End M.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
index 505c5ce378..a961330b81 100644
--- a/test-suite/output/ErrorInSection.v
+++ b/test-suite/output/ErrorInSection.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-vio") -*- *)
 Section S.
   Definition foo := nonexistent.
 End S.
diff --git a/test-suite/output/ExtractionString.out b/test-suite/output/ExtractionString.out
new file mode 100644
index 0000000000..2a101d9cea
--- /dev/null
+++ b/test-suite/output/ExtractionString.out
@@ -0,0 +1,52 @@
+(** val str : string **)
+
+let str =
+  String ((Ascii (False, False, True, False, True, False, True, False)),
+    (String ((Ascii (False, False, False, True, False, True, True, False)),
+    (String ((Ascii (True, False, False, True, False, True, True, False)),
+    (String ((Ascii (True, True, False, False, True, True, True, False)),
+    (String ((Ascii (False, False, False, False, False, True, False, False)),
+    (String ((Ascii (True, False, False, True, False, True, True, False)),
+    (String ((Ascii (True, True, False, False, True, True, True, False)),
+    (String ((Ascii (False, False, False, False, False, True, False, False)),
+    (String ((Ascii (True, False, False, False, False, True, True, False)),
+    (String ((Ascii (False, False, False, False, False, True, False, False)),
+    (String ((Ascii (True, True, False, False, True, True, True, False)),
+    (String ((Ascii (False, False, True, False, True, True, True, False)),
+    (String ((Ascii (False, True, False, False, True, True, True, False)),
+    (String ((Ascii (True, False, False, True, False, True, True, False)),
+    (String ((Ascii (False, True, True, True, False, True, True, False)),
+    (String ((Ascii (True, True, True, False, False, True, True, False)),
+    EmptyString)))))))))))))))))))))))))))))))
+str :: String
+str =
+  String0 (Ascii False False True False True False True False) (String0
+    (Ascii False False False True False True True False) (String0 (Ascii True
+    False False True False True True False) (String0 (Ascii True True False
+    False True True True False) (String0 (Ascii False False False False False
+    True False False) (String0 (Ascii True False False True False True True
+    False) (String0 (Ascii True True False False True True True False)
+    (String0 (Ascii False False False False False True False False) (String0
+    (Ascii True False False False False True True False) (String0 (Ascii
+    False False False False False True False False) (String0 (Ascii True True
+    False False True True True False) (String0 (Ascii False False True False
+    True True True False) (String0 (Ascii False True False False True True
+    True False) (String0 (Ascii True False False True False True True False)
+    (String0 (Ascii False True True True False True True False) (String0
+    (Ascii True True True False False True True False)
+    EmptyString)))))))))))))))
+
+
+(** val str : char list **)
+
+let str =
+  'T'::('h'::('i'::('s'::(' '::('i'::('s'::(' '::('a'::(' '::('s'::('t'::('r'::('i'::('n'::('g'::[])))))))))))))))
+(** val str : string **)
+
+let str =
+  "This is a string"
+str :: Prelude.String
+str =
+  "This is a string"
+
+
diff --git a/test-suite/output/ExtractionString.v b/test-suite/output/ExtractionString.v
new file mode 100644
index 0000000000..e4b9d22b38
--- /dev/null
+++ b/test-suite/output/ExtractionString.v
@@ -0,0 +1,25 @@
+Require Import String Extraction.
+
+Definition str := "This is a string"%string.
+
+(* Raw extraction of strings, in OCaml *)
+Extraction Language OCaml.
+Extraction str.
+
+(* Raw extraction of strings, in Haskell *)
+Extraction Language Haskell.
+Extraction str.
+
+(* Extraction to char list, in OCaml *)
+Require Import ExtrOcamlString.
+Extraction Language OCaml.
+Extraction str.
+
+(* Extraction to native strings, in OCaml *)
+Require Import ExtrOcamlNativeString.
+Extraction str.
+
+(* Extraction to native strings, in Haskell *)
+Require Import ExtrHaskellString.
+Extraction Language Haskell.
+Extraction str.
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index e6d674c1e6..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2).
 Check s0.
 Check s1.
 Check s2.
+
+Section Y.
+  Let s3 := MKL x3.
+  Canonical Structure s3.
+  Check (refl_equal _ : l _ = x3).
+End Y.
+Fail Check (refl_equal _ : l _ = x3).
+Fail Check s3.
+
+Section V.
+  #[canonical] Let s3 := MKL x3.
+  Check (refl_equal _ : l _ = x3).
+End V.
+
+Section W.
+  #[canonical, local] Definition s2' := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+End W.
+Fail Check (refl_equal _ : l _ = x2).
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 804f79c289..4b2d4457bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -204,3 +204,19 @@ End NonRecLetIn.
 
 Fail Inductive foo (T : Type) : let T := Type in T :=
   { r : forall x : T, x = x }.
+
+Module Discharge.
+  (* discharge test *)
+  Section S.
+    Let x := Prop.
+    Inductive foo : x := bla : foo.
+  End S.
+  Check bla:foo.
+
+  Section S.
+    Variables (A:Type).
+    (* ensure params are scanned for needed section variables even with template arity *)
+    #[universes(template)] Inductive bar (d:A) := .
+  End S.
+  Check @bar nat 0.
+End Discharge.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 1b04594290..1122b9fa34 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,28 +109,37 @@ match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
 
-(* let ins should be supported in the type of the specialized hypothesis *)
-Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False.
+
+(* let ins should be supported int he type of the specialized hypothesis *)
+Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False).
 Goal False.
   pose proof foo as P.
   assert (2 = 2) as A by reflexivity.
+  (* specialize P with (m2:= 2). *)
   specialize P with (1 := A).
+  match type of P with
+  | let n := 2 * 2 in False => idtac
+  | _ => fail "test failed"
+  end.
   assumption.
 Qed.
 
 (* Another more subtle test on letins: they should not interfere with foralls. *)
-Goal forall (P: forall y:nat,
-                forall A (zz:A),
-                  let a := zz in
-                  let x := 1 in
-                  forall n : y = x,
-                    n = n),
+Goal forall (P: forall a c:nat,
+                  let b := c in
+                  let d := 1 in
+                  forall n : a = d, a = c+1),
     True.
   intros P.
-  specialize P with (zz := @eq_refl _ 2).
+  specialize P with (1:=eq_refl).
+  match type of P with
+  | forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac
+  | _ => fail "test failed"
+  end.
   constructor.
 Qed.
 
+
 (* Test specialize as *)
 
 Goal (forall x, x=0) -> 1=0.