Files

 master

/

refman

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

maximedenes

Merge PR rocq-prover#1080: Remove some unused parts of the reference …

Oct 3, 2017

9bcfb39 · Oct 3, 2017

History

History

This branch is 22952 commits behind rocq-prover/rocq:master.

/

refman

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
AddRefMan-pre.tex		AddRefMan-pre.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
AsyncProofs.tex		AsyncProofs.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
CanonicalStructures.tex		CanonicalStructures.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Cases.tex		Cases.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Classes.tex		Classes.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Coercion.tex		Coercion.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Extraction.tex		Extraction.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Micromega.tex		Micromega.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Misc.tex		Misc.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Nsatz.tex		Nsatz.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Omega.tex		Omega.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Polynom.tex		Polynom.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Program.tex		Program.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-cic.tex		RefMan-cic.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-com.tex		RefMan-com.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-ext.tex		RefMan-ext.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-gal.tex		RefMan-gal.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-ide.tex		RefMan-ide.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-int.tex		RefMan-int.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-lib.tex		RefMan-lib.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-ltac.tex		RefMan-ltac.tex	[vernac] Remove Qed exporting syntax.	Sep 29, 2017
RefMan-mod.tex		RefMan-mod.tex	Fix various typos in documentation	Mar 31, 2015
RefMan-modr.tex		RefMan-modr.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-oth.tex		RefMan-oth.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-pre.tex		RefMan-pre.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-pro.tex		RefMan-pro.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-sch.tex		RefMan-sch.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-ssr.tex		RefMan-ssr.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-syn.tex		RefMan-syn.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-tac.tex		RefMan-tac.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-tacex.tex		RefMan-tacex.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
RefMan-uti.tex		RefMan-uti.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Reference-Manual.tex		Reference-Manual.tex	Port ssr manual to Coq's latex/hevea style	Aug 2, 2017
Setoid.tex		Setoid.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
Universes.tex		Universes.tex	Avoid generated names for html pages of the reference manual (bug roc…	Sep 22, 2017
biblio.bib		biblio.bib	update Proof General URL	Aug 23, 2016
coq-listing.tex		coq-listing.tex	Port ssr manual to Coq's latex/hevea style	Aug 2, 2017
coqdoc.tex		coqdoc.tex	Documenting how to support some special unicode characters in coqdoc	Sep 26, 2015
coqide-queries.png		coqide-queries.png	Nettoyage de l'archive doc et restructuration avant intégration à l'a…	Feb 23, 2006
coqide.png		coqide.png	Nettoyage de l'archive doc et restructuration avant intégration à l'a…	Feb 23, 2006
headers.hva		headers.hva	Make sure that hyperref creates the proper links to the documentation…	Apr 2, 2015
headers.sty		headers.sty	Make sure that hyperref creates the proper links to the documentation…	Apr 2, 2015
hevea.sty		hevea.sty	Nettoyage de l'archive doc et restructuration avant intégration à l'a…	Feb 23, 2006
index.html		index.html	Changement du index.html généré dans refman	Jun 13, 2006
menu.html		menu.html	Separate index for vernacular options.	Feb 17, 2015
View all files