12 files changed, 140 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/5434.v b/test-suite/bugs/closed/5434.v
new file mode 100644
index 000000000..5d2460fac
--- /dev/null
+++ b/test-suite/bugs/closed/5434.v
@@ -0,0 +1,18 @@
+(* About binders which remain unnamed after typing *)
+
+Global Set Asymmetric Patterns.
+
+Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x :
+@sig A P) : @sig A Q
+  := let 'exist a p := x in exist Q a (f a p).
+Axioms (feBW' : Type) (g : Prop -> Prop) (f' : feBW' -> Prop).
+Definition foo := @proj2_sig_map feBW' (fun  H  => True = f' _) (fun H =>
+ g True = g (f' H))
+                                 (fun (a : feBW') (p : (fun H : feBW' => True =
+ f' H) a) => @f_equal Prop Prop g True (f' a) p).
+Print foo.
+Goal True.
+  lazymatch type of foo with
+  | sig (fun a : ?A => ?P) -> _
+    => pose (fun a : A => a = a /\ P = P)
+  end.
diff --git a/test-suite/bugs/closed/5713.v b/test-suite/bugs/closed/5713.v
new file mode 100644
index 000000000..9daf9647f
--- /dev/null
+++ b/test-suite/bugs/closed/5713.v
@@ -0,0 +1,15 @@
+(* Checking that classical_right/classical_left work in an empty context *)
+
+Require Import Classical.
+
+Parameter A:Prop.
+
+Goal A \/ ~A.
+classical_right.
+assumption.
+Qed.
+
+Goal ~A \/ A.
+classical_left.
+assumption.
+Qed.
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
index 31cf11665..1615bfd06 100644
--- a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
@@ -1,7 +1,7 @@
 -include ../../Makefile.conf
 
-CO=$(COQMF_OCAMLFIND) opt
-CB=$(COQMF_OCAMLFIND) ocamlc
+CO="$(COQMF_OCAMLFIND)" opt
+CB="$(COQMF_OCAMLFIND)" ocamlc
 
 all:
 	$(CO) -c foolib.ml
diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh
index a0d8a7fea..5b24df639 100755
--- a/test-suite/coq-makefile/findlib-package/run.sh
+++ b/test-suite/coq-makefile/findlib-package/run.sh
@@ -4,6 +4,11 @@
 
 echo "let () = Foolib.foo ();;" >> src/test_aux.ml
 export OCAMLPATH=$OCAMLPATH:$PWD/findlib
+if which cygpath 2>/dev/null; then
+  # the only way I found to pass OCAMLPATH on win is to have it contain
+  # only one entry
+  export OCAMLPATH=`cygpath -w $PWD/findlib`
+fi
 make -C findlib/foo clean
 coq_makefile -f _CoqProject -o Makefile
 cat Makefile.conf
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out
new file mode 100644
index 000000000..0e05660d6
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.html.out
@@ -0,0 +1,50 @@
+<!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=iso-8859-1" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.bug5700</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug5700</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+<pre>foo (* bar *) </pre>
+ 
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+<pre>more (* nested (* comments *) within verbatim *) </pre>
+ 
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<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/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
new file mode 100644
index 000000000..33990cb89
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -0,0 +1,24 @@
+\documentclass[12pt]{report}
+\usepackage[]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.bug5700}{Library }{Coqdoc.bug5700}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+\begin{verbatim}foo (* bar *) \end{verbatim}
+ \begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol
+\coqdocemptyline
+\end{coqdoccode}
+\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim}
+ \begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v
new file mode 100644
index 000000000..839034a48
--- /dev/null
+++ b/test-suite/coqdoc/bug5700.v
@@ -0,0 +1,5 @@
+(** << foo (* bar *) >> *)
+Definition const1 := 1.
+
+(** << more (* nested (* comments *) within verbatim *) >> *)
+Definition const2 := 2.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 9d106d2da..7bcd7b041 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with
                              | 1 => 1
                              end = p
      : forall x : nat, x = x -> Prop
+bar  0
+     : nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b9985a594..fe6c05c39 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
 Notation "1" := eq_refl.
 Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.
 
+(* Check bug 5693 *)
+
+Module M.
+Definition A := 0.
+Definition bar (a b : nat) := plus a b.
+Notation "" := A (format "", only printing).
+Check (bar A 0).
+End M.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e5dbfcb4b..65efe228a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -122,3 +122,5 @@ return (1, 2, 3, 4)
      : nat * nat * nat * nat
 {{ 1 | 1 // 1 }}
      : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b1015137d..ea372ad1a 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+
+(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
+Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
+Check !!! (x y:nat), True.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 837f2efd0..4d04f2cf9 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
 Reserved Notation "x === y" (at level 50).
 Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
  where "x === y" := (EQ x y).
+
+(* Check that strictly ident or _ are coerced to a name *)
+
+Fail Check {x@{u},y|x=x}.
+Fail Check {?[n],y|0=0}.