From 8f12597c883db13abe7de3cc145d515b37d549ca Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 15 Jul 2017 00:16:38 +0200 Subject: Adding a coqdoc target to test-suite. One file was already ready for testing. We add another one. Note that we have to remove the machine-dependent lines in the output tex files. --- .gitignore | 2 + test-suite/Makefile | 35 ++++++- test-suite/coqdoc/bug5648.html.out | 60 +++++++++++ test-suite/coqdoc/bug5648.tex.out | 57 ++++++++++ test-suite/coqdoc/bug5648.v | 24 +++++ test-suite/coqdoc/links.html.out | 206 +++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/links.tex.out | 162 +++++++++++++++++++++++++++++ 7 files changed, 545 insertions(+), 1 deletion(-) create mode 100644 test-suite/coqdoc/bug5648.html.out create mode 100644 test-suite/coqdoc/bug5648.tex.out create mode 100644 test-suite/coqdoc/bug5648.v create mode 100644 test-suite/coqdoc/links.html.out create mode 100644 test-suite/coqdoc/links.tex.out diff --git a/.gitignore b/.gitignore index 5340f081d..9081df362 100644 --- a/.gitignore +++ b/.gitignore @@ -74,6 +74,8 @@ test-suite/coq-makefile/*/subdir/done test-suite/coq-makefile/merlin1/.merlin test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject +test-suite/coqdoc/Coqdoc.* +test-suite/coqdoc/index.html # documentation diff --git a/test-suite/Makefile b/test-suite/Makefile index 5ab4cacda..ca2decefa 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,6 +33,7 @@ BIN := $(LIB)/bin/ coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source @@ -85,7 +86,8 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm + output-modulo-time interactive micromega $(COMPLEXITY) modules stm \ + coqdoc # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile @@ -153,6 +155,7 @@ summary: $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ $(call summary_dir, "Coq makefile", coq-makefile); \ + $(call summary_dir, "Coqdoc tests", coqdoc); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -455,6 +458,8 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) fi; \ } > "$@" +# vio compilation + vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @@ -472,6 +477,8 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) fi; \ } > "$@" +# coqchk + coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @@ -488,6 +495,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) fi; \ } > "$@" +# coq_makefile + coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh @@ -504,3 +513,27 @@ coq-makefile/%.log : coq-makefile/%/run.sh echo " $<...Error!"; \ fi; \ ) > "$@" + +# 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){ \ + echo $(call log_intro,$<); \ + $(coqc) -R coqdoc Coqdoc $* 2>&1; \ + cd coqdoc; \ + f=`basename $*`; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ + grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \ + if [ $$R = 0 -a $$S = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + fi; \ + } > "$@" diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out new file mode 100644 index 000000000..f602e9859 --- /dev/null +++ b/test-suite/coqdoc/bug5648.html.out @@ -0,0 +1,60 @@ + + + + + +Coqdoc.bug5648 + + + + +
+ + + +
+ +

Library Coqdoc.bug5648

+ +
+Lemma a : True.
+Proof.
+auto.
+Qed.
+ +
+Variant t :=
+| A | Add | G | Goal | L | Lemma | P | Proof .
+ +
+Definition d x :=
+  match x with
+  | A => 0
+  | Add => 1
+  | G => 2
+  | Goal => 3
+  | L => 4
+  | Lemma => 5
+  | P => 6
+  | Proof => 7
+  end.
+ +
+Ltac Next := easy.
+ +
+Lemma yes : True.
+Proof. Next. Qed.
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out new file mode 100644 index 000000000..bb4c12be7 --- /dev/null +++ b/test-suite/coqdoc/bug5648.tex.out @@ -0,0 +1,57 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5648}{Library }{Coqdoc.bug5648} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.a}{a}{\coqdoclemma{a}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol +\coqdocnoindent +\coqdockw{Proof}.\coqdoceol +\coqdocnoindent +\coqdoctac{auto}.\coqdoceol +\coqdocnoindent +\coqdockw{Qed}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Variant} \coqdef{Coqdoc.bug5648.t}{t}{\coqdocinductive{t}} :=\coqdoceol +\coqdocnoindent +\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 +\coqdocindent{1.00em} +\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Add}{\coqdocconstructor{Add}} \ensuremath{\Rightarrow} 1\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.G}{\coqdocconstructor{G}} \ensuremath{\Rightarrow} 2\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Goal}{\coqdocconstructor{Goal}} \ensuremath{\Rightarrow} 3\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.L}{\coqdocconstructor{L}} \ensuremath{\Rightarrow} 4\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Lemma}{\coqdocconstructor{Lemma}} \ensuremath{\Rightarrow} 5\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.P}{\coqdocconstructor{P}} \ensuremath{\Rightarrow} 6\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Proof}{\coqdocconstructor{Proof}} \ensuremath{\Rightarrow} 7\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Ltac} \coqdockw{Next} := \coqdocvar{easy}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.yes}{yes}{\coqdoclemma{yes}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol +\coqdocnoindent +\coqdockw{Proof}. \coqdockw{Next}. \coqdockw{Qed}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v new file mode 100644 index 000000000..353ecc49a --- /dev/null +++ b/test-suite/coqdoc/bug5648.v @@ -0,0 +1,24 @@ +Lemma a : True. +Proof. +auto. +Qed. + +Variant t := +| A | Add | G | Goal | L | Lemma | P | Proof . + +Definition d x := + match x with + | A => 0 + | Add => 1 + | G => 2 + | Goal => 3 + | L => 4 + | Lemma => 5 + | P => 6 + | Proof => 7 + end. + +Ltac Next := easy. + +Lemma yes : True. +Proof. Next. Qed. diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out new file mode 100644 index 000000000..7d7d01c1b --- /dev/null +++ b/test-suite/coqdoc/links.html.out @@ -0,0 +1,206 @@ + + + + + +Coqdoc.links + + + + +
+ + + +
+ +

Library Coqdoc.links

+ +
+
+ +
+Various checks for coqdoc + +
+ +
    +
  • symbols should not be inlined in string g + +
    • +
  • links to both kinds of notations in a' should work to the right notation + +
    • +
  • with utf8 option, forall must be unicode + +
    • +
  • splitting between symbols and ident should be correct in a' and c + +
    • +
  • ".." should be rendered correctly + +
    • +
+ +
+
+ +
+Require Import String.
+ +
+Definition g := "dfjkh""sdfhj forall <> * ~"%string.
+ +
+Definition a (b: nat) := b.
+ +
+Definition f := forall C:Prop, C.
+ +
+Notation "n ++ m" := (plus n m).
+ +
+Notation "n ++ m" := (mult n m). +
+Notation "n ** m" := (plus n m) (at level 60).
+ +
+Notation "n ▵ m" := (plus n m) (at level 60).
+ +
+Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
+ +
+Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A
+
+where "x = y :> A" := (@eq A x y) : type_scope.
+ +
+Definition eq0 := 0 = 0 :> nat.
+ +
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+ +
+Definition b_α := ((0#0;0) , (0 ** 0)).
+ +
+Notation h := a.
+ +
+  Section test.
+ +
+    Variables b' b2: nat.
+ +
+    Notation "n + m" := (n ▵ m) : my_scope.
+ +
+    Delimit Scope my_scope with my.
+ +
+    Notation l := 0.
+ +
+    Definition α := (0 + l)%my.
+ +
+    Definition a' b := b'++0++b2 _ ++x b.
+ +
+    Definition c := {True}+{True}.
+ +
+    Definition d := (1+2)%nat.
+ +
+    Lemma e : nat + nat.
+    Admitted.
+ +
+  End test.
+ +
+  Section test2.
+ +
+    Variables b': nat.
+ +
+    Section test.
+ +
+      Variables b2: nat.
+ +
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+ +
+    End test.
+ +
+  End test2.
+ +
+
+ +
+skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+ + skip +
+
+ +
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out new file mode 100644 index 000000000..844fb3031 --- /dev/null +++ b/test-suite/coqdoc/links.tex.out @@ -0,0 +1,162 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.links}{Library }{Coqdoc.links} + +\begin{coqdoccode} +\end{coqdoccode} +Various checks for coqdoc + + + +\begin{itemize} +\item symbols should not be inlined in string g + +\item links to both kinds of notations in a' should work to the right notation + +\item with utf8 option, forall must be unicode + +\item splitting between symbols and ident should be correct in a' and c + +\item ``..'' should be rendered correctly + +\end{itemize} +\begin{coqdoccode} +\coqdocemptyline +\coqdocnoindent +\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/stdlib/Coq.Strings.String}{\coqdoclibrary{String}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\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 +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \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 +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \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}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\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 +\coqdocnoindent +\coqdoceol +\coqdocnoindent +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{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 +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\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 +\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 +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocindent{2.00em} +\coqdocvar{Admitted}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2}{test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test2.b'}{b'}{\coqdocvariable{b'}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{3.00em} +\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 +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip \begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\end{document} -- cgit v1.2.3