15 files changed, 462 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v
new file mode 100644
index 0000000000..82a317b250
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11816.v
@@ -0,0 +1,2 @@
+(* This should be an error, not an anomaly *)
+Fail Definition foo := fix foo (n : nat) { wf n n } := 0.
diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v
new file mode 100644
index 0000000000..9831a4d205
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13278.v
@@ -0,0 +1,15 @@
+Inductive even: nat -> Prop :=
+| evenB: even 0
+| evenS: forall n, even n -> even (S (S n)).
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a with end).
+Qed.
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a in even n
+                   return match n with 1 => False | _ => True end : Prop
+                   with evenB => I | evenS _ _ => I end).
+Qed.
diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out
index 2b5648aee6..aceccc25fd 100644
--- a/test-suite/coqdoc/binder.tex.out
+++ b/test-suite/coqdoc/binder.tex.out
@@ -20,7 +20,8 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-Link binders \begin{coqdoccode}
+Link binders 
+\begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
index d7eba096fc..a8f4c254cb 100644
--- a/test-suite/coqdoc/bug12742.tex.out
+++ b/test-suite/coqdoc/bug12742.tex.out
@@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
           xxxxx xxxx xxxxxx.
 
 \end{itemize}
+
 \begin{coqdoccode}
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out
index 286e8bba4d..84214a73d3 100644
--- a/test-suite/coqdoc/bug5700.html.out
+++ b/test-suite/coqdoc/bug5700.html.out
@@ -22,8 +22,7 @@
 </div>
 
 <div class="doc">
-<pre>foo (* bar *) </pre>
- 
+<code> foo (* {bar_bar} *) </code> 
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/>
@@ -32,8 +31,7 @@
 </div>
 
 <div class="doc">
-<pre>more (* nested (* comments *) within verbatim *) </pre>
- 
+<code> more (* nested (* comments *) within verbatim *) </code> 
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/>
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
index 1a1af5dfdd..f2b12f0079 100644
--- a/test-suite/coqdoc/bug5700.tex.out
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -20,14 +20,14 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-\begin{verbatim}foo (* bar *) \end{verbatim}
- \begin{coqdoccode}
+\texttt{ foo (* \{bar\_bar\} *) } 
+\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}
+\texttt{ more (* nested (* comments *) within verbatim *) } 
+\begin{coqdoccode}
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
 \end{coqdoccode}
diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v
index 839034a48f..fc985276af 100644
--- a/test-suite/coqdoc/bug5700.v
+++ b/test-suite/coqdoc/bug5700.v
@@ -1,4 +1,4 @@
-(** << foo (* bar *) >> *)
+(** << foo (* {bar_bar} *) >> *)
 Definition const1 := 1.
 
 (** << more (* nested (* comments *) within verbatim *) >> *)
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 2304f5ecc1..412a9ca6ac 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -36,6 +36,7 @@ Various checks for coqdoc
 \item  ``..'' should be rendered correctly
 
 \end{itemize}
+
 \begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
@@ -166,7 +167,8 @@ skip
 
  skip 
 
- skip \begin{coqdoccode}
+ skip 
+\begin{coqdoccode}
 \coqdocemptyline
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out
new file mode 100644
index 0000000000..bf9f975ee8
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.html.out
@@ -0,0 +1,114 @@
+<!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.verbatim</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.verbatim</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+
+<div class="paragraph"> </div>
+
+<pre>
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a &gt;&gt; shift;
+}
+</pre>
+
+<div class="paragraph"> </div>
+
+This line and the following shows <code>verbatim </code> text:
+
+<div class="paragraph"> </div>
+
+<code> A stand-alone inline verbatim </code>
+
+<div class="paragraph"> </div>
+
+<code> A non-ended inline verbatim to test line location
+</code>
+
+<div class="paragraph"> </div>
+
+<ul class="doclist">
+<li> item 1
+
+</li>
+<li> item 2 is <code>verbatim</code>
+
+</li>
+<li> item 3 is <code>verbatim</code> too
+<br/>
+<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0
+<div class="paragraph"> </div>
+
+</span>
+</li>
+<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span>
+
+</li>
+<li>
+<pre>
+multiline
+verbatim
+</pre>
+
+</li>
+<li> last item
+
+</li>
+</ul>
+
+<div class="paragraph"> </div>
+
+<center><table class="infrule">
+<tr class="infruleassumption">
+  <td class="infrule">Γ ⊢ A</td>
+  <td class="infrulenamecol" rowspan="3">
+    &nbsp;
+  </td></tr>
+<tr class="infrulemiddle">
+  <td class="infrule"><hr /></td>
+</tr>
+<tr class="infruleassumption">
+  <td class="infrule">Γ ⊢ A ∨ B</td>
+  <td></td>
+</td>
+</table></center>
+<div class="paragraph"> </div>
+
+<pre>
+A non-ended block verbatim to test line location
+
+*)
+</pre>
+</div>
+<div class="code">
+</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/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out
new file mode 100644
index 0000000000..b692f6ad6a
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.tex.out
@@ -0,0 +1,84 @@
+\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.verbatim}{Library }{Coqdoc.verbatim}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+
+
+\begin{verbatim}
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+\end{verbatim}
+
+
+This line and the following shows \texttt{verbatim } text:
+
+
+\texttt{ A stand-alone inline verbatim }
+
+
+\texttt{ A non-ended inline verbatim to test line location
+}
+
+
+
+\begin{itemize}
+\item  item 1
+
+\item  item 2 is \texttt{verbatim}
+
+\item  item 3 is \texttt{verbatim} too
+\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0
+
+\coqdocemptyline
+
+\item  \texttt{verbatim} again, and a formula  \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} 
+
+\item 
+\begin{verbatim}
+multiline
+verbatim
+\end{verbatim}
+
+\item  last item
+
+\end{itemize}
+
+
+\begin{verbatim}
+Γ ⊢ A
+----
+Γ ⊢ A ∨ B
+\end{verbatim}
+
+
+\begin{verbatim}
+A non-ended block verbatim to test line location
+
+*)
+\end{verbatim}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v
new file mode 100644
index 0000000000..129a5117c9
--- /dev/null
+++ b/test-suite/coqdoc/verbatim.v
@@ -0,0 +1,40 @@
+(**
+
+<<
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+>>
+
+This line and the following shows << verbatim >> text:
+
+<< A stand-alone inline verbatim >>
+
+<< A non-ended inline verbatim to test line location
+
+
+- item 1
+- item 2 is <<verbatim>>
+- item 3 is <<verbatim>> too
+[[
+A coq block : forall n, n = 0
+]]
+- <<verbatim>> again, and a formula [ True -> False ]
+-
+<<
+multiline
+verbatim
+>>
+- last item
+
+[[[
+Γ ⊢ A
+----
+Γ ⊢ A ∨ B
+]]]
+
+<<
+A non-ended block verbatim to test line location
+
+*)
diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out
new file mode 100644
index 0000000000..37a0613b25
--- /dev/null
+++ b/test-suite/output/HintLocality.out
@@ -0,0 +1,92 @@
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v
new file mode 100644
index 0000000000..4481335907
--- /dev/null
+++ b/test-suite/output/HintLocality.v
@@ -0,0 +1,72 @@
+(** Test hint command locality w.r.t. modules *)
+
+Create HintDb foodb.
+Create HintDb bardb.
+Create HintDb quxdb.
+
+#[global] Hint Immediate O : foodb.
+#[global] Hint Immediate O : bardb.
+#[global] Hint Immediate O : quxdb.
+
+Module Test.
+
+#[global] Hint Cut [ _ ] : foodb.
+#[global] Hint Mode S ! : foodb.
+#[global] Hint Opaque id : foodb.
+#[global] Remove Hints O : foodb.
+
+#[local] Hint Cut [ _ ] : bardb.
+#[local] Hint Mode S ! : bardb.
+#[local] Hint Opaque id : bardb.
+#[local] Remove Hints O : bardb.
+
+#[export] Hint Cut [ _ ] : quxdb.
+#[export] Hint Mode S ! : quxdb.
+#[export] Hint Opaque id : quxdb.
+#[export] Remove Hints O : quxdb.
+
+(** All three agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+End Test.
+
+(** bardb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+Import Test.
+
+(** foodb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+(** Test hint command locality w.r.t. sections *)
+
+Create HintDb secdb.
+
+#[global] Hint Immediate O : secdb.
+
+Section Sec.
+
+Fail #[global] Hint Cut [ _ ] : secdb.
+Fail #[global] Hint Mode S ! : secdb.
+Fail #[global] Hint Opaque id : secdb.
+Fail #[global] Remove Hints O : secdb.
+
+#[local] Hint Cut [ _ ] : secdb.
+#[local] Hint Mode S ! : secdb.
+#[local] Hint Opaque id : secdb.
+#[local] Remove Hints O : secdb.
+
+Print HintDb secdb.
+
+End Sec.
+
+Print HintDb secdb.
diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out
new file mode 100644
index 0000000000..034830f1ac
--- /dev/null
+++ b/test-suite/output/bug_13266.out
@@ -0,0 +1,12 @@
+The command has indeed failed with message:
+Abstracting over the terms "S", "p" and "u" leads to a term
+fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True
+which is ill-typed.
+Reason is: Illegal application: 
+The term "@eq" of type "forall A : Type, A -> A -> Prop"
+cannot be applied to the terms
+ "proc S0" : "Prop"
+ "p0" : "proc S0"
+ "Tick" : "proc unit"
+The 3rd term has type "proc unit" which should be coercible to 
+"proc S0".
diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v
new file mode 100644
index 0000000000..e59455a326
--- /dev/null
+++ b/test-suite/output/bug_13266.v
@@ -0,0 +1,18 @@
+Inductive proc : Type -> Type :=
+| Tick : proc unit
+.
+
+Inductive exec :
+  forall T, proc T -> T -> Prop :=
+| ExecTick :
+    exec _ (Tick) tt
+.
+
+Lemma foo :
+  exec _ Tick tt ->
+  True.
+Proof.
+  intros H. 
+  remember Tick as p.
+  Fail induction H.
+Abort.