\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.bug11194}{Library }{Coqdoc.bug11194} \begin{coqdoccode} \coqdocnoindent \coqdockw{Record} \coqdef{Coqdoc.bug11194.a struct}{a\_struct}{\coqdocrecord{a\_struct}} := \{ \coqdef{Coqdoc.bug11194.anum}{anum}{\coqdocprojection{anum}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \}.\coqdoceol \coqdocnoindent \coqdockw{Canonical} \coqdockw{Structure} \coqdef{Coqdoc.bug11194.a struct 0}{a\_struct\_0}{\coqdocdefinition{a\_struct\_0}} := \{| \coqref{Coqdoc.bug11194.anum}{\coqdocprojection{anum}} := 0|\}.\coqdoceol \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug11194.rename a s 0}{rename\_a\_s\_0}{\coqdocdefinition{rename\_a\_s\_0}} := \coqref{Coqdoc.bug11194.a struct 0}{\coqdocdefinition{a\_struct\_0}}.\coqdoceol \coqdocnoindent \coqdockw{Coercion} \coqdef{Coqdoc.bug11194.some nat}{some\_nat}{\coqdocdefinition{some\_nat}} := (@\coqexternalref{Some}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}).\coqdoceol \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug11194.rename some nat}{rename\_some\_nat}{\coqdocdefinition{rename\_some\_nat}} := \coqref{Coqdoc.bug11194.some nat}{\coqdocdefinition{some\_nat}}.\coqdoceol \end{coqdoccode} \end{document}