5 files changed, 86 insertions, 2 deletions
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
index 31cf116652..1615bfd067 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 a0d8a7fea7..5b24df6397 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 0000000000..0e05660d6c
--- /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 0000000000..33990cb89f
--- /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 0000000000..839034a48f
--- /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.