18 files changed, 403 insertions, 103 deletions

diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md
index aec6cd0a21..c564105c9c 100644
--- a/.github/ISSUE_TEMPLATE.md
+++ b/.github/ISSUE_TEMPLATE.md
@@ -3,7 +3,9 @@
 #### Description of the problem
 
 <!-- If you can, it's helpful to provide self-contained example of some code
-that reproduces the bug. If not, a link to a larger example is also helpful. -->
+that reproduces the bug. If not, a link to a larger example is also helpful.
+You can generate a shorter version of your program by following these
+instructions: https://github.com/coq/coq/wiki/Coqbot-minimize-feature.  -->
 
 #### Coq Version
 
diff --git a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst
new file mode 100644
index 0000000000..a05829b720
--- /dev/null
+++ b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Special symbols now escaped in the index produced by coqdoc,
+  avoiding collision with the syntax of the output format
+  (`#12754 <https://github.com/coq/coq/pull/12754>`_,
+  fixes `#12752 <https://github.com/coq/coq/issues/12752>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst
new file mode 100644
index 0000000000..67ee061285
--- /dev/null
+++ b/doc/changelog/08-tools/12772-fix-details.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  The `details` environment added in the 8.12 release can now be used
+  as advertised in the reference manual
+  (`#12772 <https://github.com/coq/coq/pull/12772>`_,
+  by Thomas Letan).
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7b3670164b..3b4b80ca21 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2280,7 +2280,7 @@ to the others.
 Iteration
 ~~~~~~~~~
 
-.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
+.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] }
    :name: do (ssreflect)
 
    This tactical offers an accurate control on the repetition of tactics.
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 4dd7fe7e70..1c7e716fc2 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -85,12 +85,33 @@ let lower_of_list l =
 
 type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
 
-exception Found of Level.t * lowermap
-let find_inst insts v =
-  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
-    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
-        insts; raise Not_found
-  with Found (f,l) -> (f,l)
+module LBMap :
+sig
+  type t = private { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t }
+  val empty : t
+  val add : Level.t -> lbound -> t -> t
+end =
+struct
+  type t = { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t }
+  (* lbrev is uniquely given from lbmap as a partial reverse mapping *)
+  let empty = { lbmap = LMap.empty; lbrev = Universe.Map.empty }
+  let add u bnd m =
+    let lbmap = LMap.add u bnd m.lbmap in
+    let lbrev =
+      if not bnd.alg && bnd.enforce then
+        match Universe.Map.find bnd.lbound m.lbrev with
+        | (v, _) ->
+          if Level.compare u v <= 0 then
+            Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev
+          else m.lbrev
+        | exception Not_found ->
+          Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev
+      else m.lbrev
+    in
+    { lbmap; lbrev }
+end
+
+let find_inst insts v = Universe.Map.find v insts.LBMap.lbrev
 
 let compute_lbound left =
  (* The universe variable was not fixed yet.
@@ -114,11 +135,11 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts,
     let inst = Universe.make u in
     let cstrs' = enforce_leq lbound inst cstrs in
       (ctx, us, LSet.remove u algs,
-       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+       LBMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
       {enforce; alg; lbound=inst; lower}
   else (* Actually instantiate *)
     (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+     LBMap.add u {enforce;alg;lbound;lower} insts, cstrs),
     {enforce; alg; lbound; lower}
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
@@ -180,10 +201,10 @@ let minimize_univ_variables ctx us algs left right cstrs =
         let lbounds =
           match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
           | None -> lbounds
-          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
+          | Some lbound -> LBMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
                                    lbounds
         in (Univ.LMap.remove r left, lbounds))
-      left (left, Univ.LMap.empty)
+      left (left, LBMap.empty)
   in
   let rec instance (ctx, us, algs, insts, cstrs as acc) u =
     let acc, left, lower =
@@ -256,7 +277,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
         with UpperBoundedAlg ->
           enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
   and aux (ctx, us, algs, seen, cstrs as acc) u =
-    try acc, LMap.find u seen
+    try acc, LMap.find u seen.LBMap.lbmap
     with Not_found -> instance acc u
   in
     LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
index c68fab5296..3996d7edc8 100644
--- a/tactics/ppred.mli
+++ b/tactics/ppred.mli
@@ -6,10 +6,15 @@ val pr_with_occurrences :
 val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 
-val pr_red_expr_env : Environ.env -> Evd.evar_map ->
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+val pr_red_expr : ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> (string -> Pp.t) ->
+  ('a,'b,'c) red_expr_gen -> Pp.t
+
+(** Compared to [pr_red_expr], this immediately applied the tuple
+   elements to the extra arguments. *)
+val pr_red_expr_env : 'env -> 'sigma ->
+  ('env -> 'sigma -> 'a -> Pp.t) *
+  ('env -> 'sigma -> 'a -> Pp.t) *
   ('b -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
+  ('env -> 'sigma -> 'c -> Pp.t) ->
   (string -> Pp.t) ->
   ('a,'b,'c) red_expr_gen -> Pp.t
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 0935617fbf..f7447d6cec 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -771,8 +771,6 @@ coq-makefile/%.log : coq-makefile/%/run.sh
 
 # coqdoc
 
-coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh))
-
 $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v
new file mode 100644
index 0000000000..22d95949bb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12566_1.v
@@ -0,0 +1,16 @@
+
+Class C (n:nat) := c{}.
+
+Instance c0 : C 0 := {}.
+
+Definition x := 0.
+
+Opaque x.
+
+Type _ : C x.
+(* this is maybe wrong behaviour, if it changes just update the test *)
+
+Hint Opaque x : typeclass_instances.
+Transparent x.
+
+Fail Type _ : C x.
diff --git a/test-suite/coqdoc/bug12742.html.out b/test-suite/coqdoc/bug12742.html.out
new file mode 100644
index 0000000000..75dd185ff9
--- /dev/null
+++ b/test-suite/coqdoc/bug12742.html.out
@@ -0,0 +1,67 @@
+<!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.bug12742</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug12742</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+<div class="paragraph"> </div>
+
+<ul class="doclist">
+<li> <i>Xxxxxxxxx xxxxxxx xxxxxxx</i> xxxxxxx "xxxx-xxxxxx" xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx <i>xxxx</i> xx
+          <i>xxxxx</i> (xx, xxxxxxxxx, <i>xxx'x xxxx: xxx xxx xx xxxx</i>).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+<div class="paragraph"> </div>
+
+
+</li>
+<li> <i>Xxxxx xxxxxxxxxx</i> xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+
+</li>
+</ul>
+
+</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/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
new file mode 100644
index 0000000000..d7eba096fc
--- /dev/null
+++ b/test-suite/coqdoc/bug12742.tex.out
@@ -0,0 +1,51 @@
+\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.bug12742}{Library }{Coqdoc.bug12742}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+
+
+\begin{itemize}
+\item  \textit{Xxxxxxxxx xxxxxxx xxxxxxx} xxxxxxx ``xxxx-xxxxxx'' xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx \textit{xxxx} xx
+          \textit{xxxxx} (xx, xxxxxxxxx, \textit{xxx'x xxxx: xxx xxx xx xxxx}).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+
+
+\item  \textit{Xxxxx xxxxxxxxxx} xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+
+\end{itemize}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug12742.v b/test-suite/coqdoc/bug12742.v
new file mode 100644
index 0000000000..8ce1faff00
--- /dev/null
+++ b/test-suite/coqdoc/bug12742.v
@@ -0,0 +1,20 @@
+ (** Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
+     xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx.
+     Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx
+     xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx.  Xxxxx xxxxx
+     xxxx xxxx xxx xxxxx xxxxxxxxxx:
+
+        - _Xxxxxxxxx xxxxxxx xxxxxxx_ xxxxxxx "xxxx-xxxxxx" xxxxxxxxx:
+          xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx _xxxx_ xx
+          _xxxxx_ (xx, xxxxxxxxx, _xxx'x xxxx: xxx xxx xx xxxx_).
+          Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx
+          xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx
+          xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx.  Xxxxxxxx xx xxxx
+          xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx.
+
+        - _Xxxxx xxxxxxxxxx_ xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx
+          xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx
+          xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx.  Xxxxxx xxxx xxxxx
+          xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx,
+          xxxxx xxxx xxxxxx.
+*)
diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out
new file mode 100644
index 0000000000..e1f1ad9867
--- /dev/null
+++ b/test-suite/coqdoc/details.html.out
@@ -0,0 +1,48 @@
+<!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.details</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.details</h1>
+
+<div class="code">
+</div>
+<details><div class="code">
+<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := 3.<br/>
+</div>
+</details><div class="code">
+
+<br/>
+</div>
+<details><summary>Foo bar </summary><div class="code">
+<span class="id" title="keyword">Fixpoint</span> <a id="idnat" class="idref" href="#idnat"><span class="id" title="definition">idnat</span></a> (<a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Coqdoc.details.html#idnat:2"><span class="id" title="definition">idnat</span></a> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a>)<br/>
+&nbsp;&nbsp;| 0 ⇒ 0<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+</div>
+</details><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/details.tex.out b/test-suite/coqdoc/details.tex.out
new file mode 100644
index 0000000000..37778944ba
--- /dev/null
+++ b/test-suite/coqdoc/details.tex.out
@@ -0,0 +1,44 @@
+\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.details}{Library }{Coqdoc.details}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocemptyline
+\end{coqdoccode}
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{end}.\coqdoceol
+\end{coqdoccode}
+\begin{coqdoccode}
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v
new file mode 100644
index 0000000000..208e60317d
--- /dev/null
+++ b/test-suite/coqdoc/details.v
@@ -0,0 +1,11 @@
+(* begin details *)
+Definition foo : nat := 3.
+(* end details *)
+
+(* begin details : Foo bar *)
+Fixpoint idnat (x : nat) : nat :=
+  match x with
+  | S x => S (idnat x)
+  | 0 => 0
+  end.
+(* end details *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index aa3c5b9d3b..5d210b2e60 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -504,9 +504,9 @@ rule coq_bol = parse
       { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf }
   | space* end_show nl
       { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf }
-  | space* begin_details nl
-      { Lexing.new_line lexbuf;
-        let s = details_body lexbuf in
+  | space* begin_details (* At this point, the comment remains open,
+                            and will be closed by [details_body] *)
+      { let s = details_body lexbuf in
         Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
   | space* end_details nl
       { Lexing.new_line lexbuf;
@@ -728,7 +728,7 @@ and doc_bol = parse
           else
             Output.section lev (fun () -> ignore (doc None (from_string s)));
 	    if eol then doc_bol lexbuf else doc None lexbuf }
-  | (space_nl* as s) ('-'+ as line)
+  | ((space_nl* nl)? as s) (space* '-'+ as line)
       { let nl_count = count_newlines s in
         match check_start_list line with
           | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index def1cbbcf8..32cf05e1eb 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -838,7 +838,7 @@ module Html = struct
       printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
       List.iter
         (fun (id,(text,link,t)) ->
-           let id' = prepare_entry id t in
+           let id' = escaped (prepare_entry id t) in
            printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
       printf "<br/><br/>"
     end
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 0e3e3c61a9..051560fb63 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Util
+open Names
 
 (** (Partial) implementation of the [Hint] command; some more
    functionality still lives in tactics/hints.ml *)
@@ -61,7 +62,7 @@ let project_hint ~poly pri l2r r =
       cb
   in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-  (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
+  (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
   CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -70,6 +71,16 @@ let warn_deprecated_hint_constr =
         "Declaring arbitrary terms as hints is fragile; it is recommended to \
          declare a toplevel constant instead")
 
+(* Only error when we have to (axioms may be instantiated if from functors)
+   XXX maybe error if not from a functor argument?
+ *)
+let soft_evaluable =
+  let open GlobRef in
+  function
+  | ConstRef c -> EvalConstRef c
+  | VarRef id -> EvalVarRef id
+  | (IndRef _ | ConstructRef _) as r -> Tacred.error_not_evaluable r
+
 let interp_hints ~poly h =
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -88,7 +99,7 @@ let interp_hints ~poly h =
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
     gr
   in
-  let fr r = Tacred.evaluable_of_global_reference env (fref r) in
+  let fr r = soft_evaluable (fref r) in
   let fi c =
     let open Hints in
     let open Vernacexpr in
@@ -135,7 +146,7 @@ let interp_hints ~poly h =
         "ind";
       List.init (Inductiveops.nconstructors env ind) (fun i ->
           let c = (ind, i + 1) in
-          let gr = Names.GlobRef.ConstructRef c in
+          let gr = GlobRef.ConstructRef c in
           ( empty_hint_info
           , Declareops.inductive_is_polymorphic mib
           , true
@@ -147,9 +158,7 @@ let interp_hints ~poly h =
     let pat = Option.map (fp sigma) patcom in
     let l = match pat with None -> [] | Some (l, _) -> l in
     let ltacvars =
-      List.fold_left
-        (fun accu x -> Names.Id.Set.add x accu)
-        Names.Id.Set.empty l
+      List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
     in
     let env = Genintern.{(empty_glob_sign env) with ltacvars} in
     let _, tacexp = Genintern.generic_intern env tacexp in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b93c920654..b73e7c7515 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -30,12 +30,34 @@ let tag_vernac  = do_not_tag
 
 let keyword s = tag_keyword (str s)
 
+let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
+
+let pr_in_global_env f c : Pp.t =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  f env sigma c
+
+(* when not !Flags.beautify_file these just ignore the env/sigma *)
+let pr_constr_expr = pr_in_global_env pr_constr_expr
+let pr_lconstr_expr = pr_in_global_env pr_lconstr_expr
+let pr_binders = pr_in_global_env pr_binders
+let pr_constr_pattern_expr = pr_in_global_env pr_constr_pattern_expr
+
+(* In principle this may use the env/sigma, in practice not sure if it
+   does except through pr_constr_expr in beautify mode. *)
+let pr_gen = pr_in_global_env Pputils.pr_raw_generic
+
+(* No direct Global.env or pr_in_global_env use after this *)
+
 let pr_constr = pr_constr_expr
 let pr_lconstr = pr_lconstr_expr
 let pr_spc_lconstr =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  pr_sep_com spc @@ pr_lconstr_expr env sigma
+  pr_sep_com spc @@ pr_lconstr_expr
+
+let pr_red_expr =
+  Ppred.pr_red_expr
+    (pr_constr_expr, pr_lconstr_expr, pr_smart_global, pr_constr_expr)
+    keyword
 
 let pr_uconstraint (l, d, r) =
   pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
@@ -80,8 +102,6 @@ let pr_lfqid {CAst.loc;v=fqid} =
 let pr_lname_decl (n, u) =
   pr_lname n ++ pr_universe_decl u
 
-let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
-
 let pr_ltac_ref = Libnames.pr_qualid
 
 let pr_module = Libnames.pr_qualid
@@ -100,11 +120,6 @@ let sep_end = function
   | VernacEndSubproof -> str""
   | _ -> str"."
 
-let pr_gen t =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  Pputils.pr_raw_generic env sigma t
-
 let sep = fun _ -> spc()
 let sep_v2 = fun _ -> str"," ++ spc()
 
@@ -190,9 +205,7 @@ let pr_search_where = function
 
 let pr_search_item = function
   | SearchSubPattern (where,p) ->
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    pr_search_where where ++ pr_constr_pattern_expr env sigma p
+    pr_search_where where ++ pr_constr_pattern_expr p
   | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
   | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind)
 
@@ -278,10 +291,8 @@ let pr_hints db h pr_c pr_pat =
       ++ spc() ++ prlist_with_sep spc pr_qualid c
     | HintsExtern (n,c,tac) ->
       let pat = match c with None -> mt () | Some pat -> pr_pat pat in
-      let env = Global.env () in
-      let sigma = Evd.from_env env in
       keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
-      spc() ++ Pputils.pr_raw_generic env sigma tac
+      spc() ++ pr_gen tac
   in
   hov 2 (keyword "Hint "++ pph ++ opth)
 
@@ -348,9 +359,7 @@ let pr_type_option pr_c = function
   | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
 let pr_binders_arg =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  pr_non_empty_arg @@ pr_binders env sigma
+  pr_non_empty_arg @@ pr_binders
 
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
@@ -470,21 +479,17 @@ let pr_decl_notation prc decl_ntn =
   ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
 
 let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
   let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
-  let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in
+  let annot = pr_guard_annot pr_lconstr_expr binders rec_order in
   pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot
-  ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype
-  ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def
-  ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations
+  ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) rtype
+  ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) body_def
+  ++ prlist (pr_decl_notation @@ pr_constr) notations
 
 let pr_statement head (idpl,(bl,c)) =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
   hov 2
     (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
-     (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++
+     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
      str":" ++ pr_spc_lconstr c)
 
 (**************************************)
@@ -492,13 +497,9 @@ let pr_statement head (idpl,(bl,c)) =
 (**************************************)
 
 let pr_constrarg c =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  spc () ++ pr_constr env sigma c
+  spc () ++ pr_constr c
 let pr_lconstrarg c =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  spc () ++ pr_lconstr env sigma c
+  spc () ++ pr_lconstr c
 let pr_intarg n = spc () ++ int n
 
 let pr_oc = function
@@ -507,23 +508,21 @@ let pr_oc = function
   | Some false -> str" :>>"
 
 let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
   let prx = match x with
     | AssumExpr (id,t) ->
       hov 1 (pr_lname id ++
              pr_oc oc ++ spc() ++
-             pr_lconstr_expr env sigma t)
+             pr_lconstr_expr t)
     | DefExpr(id,b,opt) -> (match opt with
         | Some t ->
           hov 1 (pr_lname id ++
                  pr_oc oc ++ spc() ++
-                 pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b)
+                 pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
         | None ->
           hov 1 (pr_lname id ++ str" :=" ++ spc() ++
-                 pr_lconstr env sigma b)) in
+                 pr_lconstr b)) in
   let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
-  prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+  prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn
 
 let pr_record_decl c fs =
   pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
@@ -650,8 +649,6 @@ let pr_extend s cl =
 
 let pr_vernac_expr v =
   let return = tag_vernac v in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
   match v with
   | VernacLoad (f,s) ->
     return (
@@ -783,7 +780,7 @@ let pr_vernac_expr v =
       | None -> mt()
       | Some r ->
         keyword "Eval" ++ spc() ++
-        Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+        pr_red_expr r ++
         keyword " in" ++ spc()
     in
     let pr_def_body = function
@@ -792,7 +789,7 @@ let pr_vernac_expr v =
           | None -> mt()
           | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty
         in
-        (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body))
+        (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body))
       | ProveBody (bl,t) ->
         let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in
         (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in
@@ -828,7 +825,7 @@ let pr_vernac_expr v =
     let n = List.length (List.flatten (List.map fst (List.map snd l))) in
     let pr_params (c, (xl, t)) =
       hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
-             (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in
+             (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
     let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
     return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
                    pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
@@ -854,9 +851,9 @@ let pr_vernac_expr v =
         (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
         pr_and_type_binders_arg indupar ++
         pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
-        pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
+        pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
         str" :=") ++ pr_constructor_list lc ++
-      prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+      prlist (pr_decl_notation @@ pr_constr) ntn
     in
     let kind =
       match f with
@@ -886,10 +883,10 @@ let pr_vernac_expr v =
       | NoDischarge -> str ""
     in
     let pr_onecorec {fname; univs; binders; rtype; body_def; notations } =
-      pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
-      spc() ++ pr_lconstr_expr env sigma rtype ++
-      pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++
-      prlist (pr_decl_notation @@ pr_constr env sigma) notations
+      pr_ident_decl (fname,univs) ++ spc() ++ pr_binders binders ++ spc() ++ str":" ++
+      spc() ++ pr_lconstr_expr rtype ++
+      pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) body_def ++
+      prlist (pr_decl_notation @@ pr_constr) notations
     in
     return (
       hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
@@ -968,11 +965,11 @@ let pr_vernac_expr v =
          | { v = Anonymous }, _ -> mt ()) ++
         pr_and_type_binders_arg sup ++
         str":" ++ spc () ++
-        pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
+        pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
         (match props with
          | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
          | Some (true,_) -> assert false
-         | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p
+         | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
          | None -> mt()))
     )
 
@@ -982,7 +979,7 @@ let pr_vernac_expr v =
         keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
         pr_and_type_binders_arg sup ++
         str":" ++ spc () ++
-        pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
+        pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
     )
 
   | VernacContext l ->
@@ -993,7 +990,7 @@ let pr_vernac_expr v =
 
   | VernacExistingInstance insts ->
     let pr_inst (id, info) =
-      pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info
+      pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
     in
     return (
       hov 1 (keyword "Existing" ++ spc () ++
@@ -1008,25 +1005,25 @@ let pr_vernac_expr v =
 
   (* Modules and Module Types *)
   | VernacDefineModule (export,m,bl,tys,bd) ->
-    let b = pr_module_binders bl (pr_lconstr env sigma) in
+    let b = pr_module_binders bl pr_lconstr in
     return (
       hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++
              pr_lident m ++ b ++
-             pr_of_module_type (pr_lconstr env sigma) tys ++
+             pr_of_module_type pr_lconstr tys ++
              (if List.is_empty bd then mt () else str ":= ") ++
              prlist_with_sep (fun () -> str " <+")
-               (pr_module_ast_inl true (pr_lconstr env sigma)) bd)
+               (pr_module_ast_inl true pr_lconstr) bd)
     )
   | VernacDeclareModule (export,id,bl,m1) ->
-    let b = pr_module_binders bl (pr_lconstr env sigma) in
+    let b = pr_module_binders bl pr_lconstr in
     return (
       hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++
              pr_lident id ++ b ++ str " :" ++
-             pr_module_ast_inl true (pr_lconstr env sigma) m1)
+             pr_module_ast_inl true pr_lconstr m1)
     )
   | VernacDeclareModuleType (id,bl,tyl,m) ->
-    let b = pr_module_binders bl (pr_lconstr env sigma) in
-    let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in
+    let b = pr_module_binders bl pr_lconstr in
+    let pr_mt = pr_module_ast_inl true pr_lconstr in
     return (
       hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++
              prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++
@@ -1034,7 +1031,7 @@ let pr_vernac_expr v =
              prlist_with_sep (fun () -> str " <+ ") pr_mt m)
     )
   | VernacInclude (mexprs) ->
-    let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in
+    let pr_m = pr_module_ast_inl false pr_lconstr in
     return (
       hov 2 (keyword "Include" ++ spc() ++
              prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
@@ -1079,7 +1076,7 @@ let pr_vernac_expr v =
              pr_opt_hintbases dbnames)
     )
   | VernacHints (dbnames,h) ->
-    return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
+    return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
   | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
     return (
       hov 2
@@ -1153,7 +1150,7 @@ let pr_vernac_expr v =
     let n = List.length (List.flatten (List.map fst bl)) in
     return (
       hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " "))
-             ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl))
+             ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
     )
   | VernacGeneralizable g ->
     return (
@@ -1221,9 +1218,9 @@ let pr_vernac_expr v =
     let pr_mayeval r c = match r with
       | Some r0 ->
         hov 2 (keyword "Eval" ++ spc() ++
-               Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
-               spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c)
-      | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c)
+               pr_red_expr r0 ++
+               spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
+      | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
     in
     let pr_i = match io with None -> mt ()
                            | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
@@ -1233,12 +1230,12 @@ let pr_vernac_expr v =
   | VernacDeclareReduction (s,r) ->
     return (
       keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
-      Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+      pr_red_expr r
     )
   | VernacPrint p ->
     return (pr_printable p)
   | VernacSearch (sea,g,sea_r) ->
-    return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma)
+    return (pr_search sea g sea_r @@ pr_constr_pattern_expr)
   | VernacLocate loc ->
     let pr_locate =function
       | LocateAny qid -> pr_smart_global qid
@@ -1270,7 +1267,7 @@ let pr_vernac_expr v =
     return (
       hov 2
         (keyword "Comments" ++ spc()
-         ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l)
+         ++ prlist_with_sep sep (pr_comment pr_constr) l)
     )
 
   (* For extension *)
@@ -1282,12 +1279,12 @@ let pr_vernac_expr v =
     return (keyword "Proof " ++ spc () ++
             keyword "using" ++ spc() ++ pr_using e)
   | VernacProof (Some te, None) ->
-    return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te)
+    return (keyword "Proof with" ++ spc() ++ pr_gen te)
   | VernacProof (Some te, Some e) ->
     return (
       keyword "Proof" ++ spc () ++
       keyword "using" ++ spc() ++ pr_using e ++ spc() ++
-      keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te
+      keyword "with" ++ spc() ++ pr_gen te
     )
   | VernacProofMode s ->
     return (keyword "Proof Mode" ++ str s)