Definition a := 0. #[
universes(
template) ]
-
Inductive mysum (
A B:
Type) :
Type :=
- |
myinl :
A → mysum A B
- |
myinr :
B → mysum A B.
+
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/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out
index a6478682d8..12ea109d0e 100644
--- a/test-suite/coqdoc/bug11353.tex.out
+++ b/test-suite/coqdoc/bug11353.tex.out
@@ -22,11 +22,11 @@
\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
+\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdef{Coqdoc.bug11353.A:1}{A}{\coqdocbinder{A}} \coqdef{Coqdoc.bug11353.B:2}{B}{\coqdocbinder{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
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\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
+\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol
diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out
index 5c5a2dc299..8201cd3ccb 100644
--- a/test-suite/coqdoc/bug5648.html.out
+++ b/test-suite/coqdoc/bug5648.html.out
@@ -29,8 +29,8 @@
|
A |
Add |
G |
Goal |
L |
Lemma |
P |
Proof .
-
Definition d x :=
-
match x with
+
Definition d x :=
+
match x with
|
A ⇒ 0
|
Add ⇒ 1
|
G ⇒ 2
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out
index 82f7da2309..c221d7ca8a 100644
--- a/test-suite/coqdoc/bug5648.tex.out
+++ b/test-suite/coqdoc/bug5648.tex.out
@@ -34,9 +34,9 @@
\ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdef{Coqdoc.bug5648.x:3}{x}{\coqdocbinder{x}} :=\coqdoceol
\coqdocindent{1.00em}
-\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol
+\coqdockw{match} \coqref{Coqdoc.bug5648.x:3}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol
\coqdocindent{1.00em}
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index d2d4d5d764..3ec5e7eb23 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -54,10 +54,10 @@ Various checks for coqdoc
Definition g := "dfjkh""sdfhj forall <> * ~"%
string.
-
Definition a (
b:
nat) :=
b.
+
Definition a (
b:
nat) :=
b.
-
Definition f :=
∀ C:
Prop,
C.
+
Definition f :=
∀ C:
Prop,
C.
Notation "n ++ m" := (
plus n m).
@@ -74,9 +74,9 @@ Various checks for coqdoc
Notation "n '_' ++ 'x' m" := (
plus n m) (
at level 3).
-
Inductive eq (
A:
Type) (
x:
A) :
A → Prop :=
eq_refl :
x = x :>A
+
Inductive eq (
A:
Type) (
x:
A) :
A → Prop :=
eq_refl :
x = x :>A
-
where "x = y :> A" := (@
eq A x y) :
type_scope.
+
where "x = y :> A" := (@
eq A x y) :
type_scope.
Definition eq0 := 0
= 0
:> nat.
@@ -109,7 +109,7 @@ Various checks for coqdoc
Definition α := (0
+ l)%
my.
-
Definition a' b :=
b'++0
++b2 _ ++x b.
+
Definition a' b :=
b'++0
++b2 _ ++x b.
Definition c :=
{True}+{True}.
@@ -137,7 +137,7 @@ Various checks for coqdoc
Variables b2:
nat.
-
Definition a'' b :=
b' ++ O ++ b2 _ ++ x b + h 0.
+
Definition a'' b :=
b' ++ O ++ b2 _ ++ x b + h 0.
End test.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 24f96ff1e6..2304f5ecc1 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -45,10 +45,10 @@ Various checks for coqdoc
\coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdef{Coqdoc.links.b:1}{b}{\coqdocbinder{b}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqref{Coqdoc.links.b:1}{\coqdocvariable{b}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdef{Coqdoc.links.C:2}{C}{\coqdocbinder{C}}:\coqdockw{Prop}, \coqref{Coqdoc.links.C:2}{\coqdocvariable{C}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
@@ -65,11 +65,11 @@ Various checks for coqdoc
\coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
+\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdef{Coqdoc.links.A:3}{A}{\coqdocbinder{A}}:\coqdockw{Type}) (\coqdef{Coqdoc.links.x:4}{x}{\coqdocbinder{x}}:\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocnoindent
-\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq:6}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
@@ -102,7 +102,7 @@ Various checks for coqdoc
\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdef{Coqdoc.links.b:9}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test.b'}{\coqdocvariable{b'}}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:9}{\coqdocvariable{b}}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
@@ -131,7 +131,7 @@ Various checks for coqdoc
\coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
\coqdocemptyline
\coqdocindent{3.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdef{Coqdoc.links.b:12}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test2.b'}{\coqdocvariable{b'}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.test2.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:12}{\coqdocvariable{b}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index dbc930f5ec..2c2bd98541 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -230,6 +230,10 @@ tr.infrulemiddle hr {
color: rgb(40%,0%,40%);
}
+.id[title="binder"] {
+ color: rgb(40%,0%,40%);
+}
+
.id[type="definition"] {
color: rgb(0%,40%,0%);
}
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index f49f9f0066..aa9c414761 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -72,6 +72,7 @@
\newcommand{\coqdocinductive}[1]{\coqdocind{#1}}
\newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}}
\newcommand{\coqdocvariable}[1]{\coqdocvar{#1}}
+\newcommand{\coqdocbinder}[1]{\coqdocvar{#1}}
\newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}}
\newcommand{\coqdoclemma}[1]{\coqdoccst{#1}}
\newcommand{\coqdocclass}[1]{\coqdocind{#1}}
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 4cc82726f1..723918525d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -31,6 +31,7 @@ type entry_type =
| Abbreviation
| Notation
| Section
+ | Binder
type index_entry =
| Def of string * entry_type
@@ -177,6 +178,7 @@ let type_name = function
| Abbreviation -> "abbreviation"
| Notation -> "notation"
| Section -> "section"
+ | Binder -> "binder"
let prepare_entry s = function
| Notation ->
@@ -268,6 +270,7 @@ let type_of_string = function
| "mod" | "modtype" -> Module
| "tac" -> TacticDefinition
| "sec" -> Section
+ | "binder" -> Binder
| s -> invalid_arg ("type_of_string:" ^ s)
let ill_formed_glob_file f =
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 3426fdd3d3..7a3d401fd7 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -30,6 +30,7 @@ type entry_type =
| Abbreviation
| Notation
| Section
+ | Binder
val type_name : entry_type -> string
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index dd1b65d294..04725aa26f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -337,11 +337,8 @@ module Latex = struct
let id = if fid <> "" then (m ^ "." ^ fid) else m in
match find_module m with
| Local ->
- if typ = Variable then
- printf "\\coqdoc%s{%s}" (type_name typ) s
- else
- (printf "\\coqref{"; label_ident id;
- printf "}{\\coqdoc%s{%s}}" (type_name typ) s)
+ printf "\\coqref{"; label_ident id;
+ printf "}{\\coqdoc%s{%s}}" (type_name typ) s
| External m when !externals ->
printf "\\coqexternalref{"; label_ident fid;
printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s
@@ -615,6 +612,7 @@ module Html = struct
else match s.[i] with
| 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1)
| '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1)
+ | '-' | ':' -> loop esc (i-1) (* should be safe in HTML5 attribute name syntax *)
| _ ->
(* This name contains complex characters:
this is probably a notation string, we simply hash it. *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 1e2e2e53e2..43e86fa9bd 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -161,7 +161,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
let env =
EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
let ienv = List.fold_right (fun {CAst.v=id} ienv ->
- let impls = compute_internalization_data env sigma Variable t imps in
+ let impls = compute_internalization_data env sigma id Variable t imps in
Id.Map.add id impls ienv) idl ienv in
((sigma,env,ienv),((is_coe,idl),t,imps)))
(sigma,env,empty_internalization_env) l
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 5b29ab2092..bf38088f71 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -196,7 +196,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let sigma, intern_body =
let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in
let interning_data =
- Constrintern.compute_internalization_data env sigma
+ Constrintern.compute_internalization_data env sigma recname
Constrintern.Recursive full_arity impls
in
let newimpls = Id.Map.singleton recname
diff --git a/vernac/record.ml b/vernac/record.ml
index b9d450044b..ac26675e6f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -71,7 +71,7 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
let impls =
match i with
| Anonymous -> impls
- | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
+ | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls
in
let d = match b' with
| None -> LocalAssum (make_annot i r,t')
--
cgit v1.2.3