index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
/
RefMan-oth.tex
Commit message (
Expand
)
Author
Age
*
sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex
Pierre Boutillier
2014-09-03
*
Update RefMan with respect to new loadpath management
Pierre Boutillier
2014-09-03
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Removing documentation related to the deprecated State machinery.
Pierre-Marie Pédrot
2014-08-16
*
Documenting the changes of Locate semantics.
Pierre-Marie Pédrot
2014-07-21
*
Fixing grammar in doc of Opaque as proposed by Jason (#3389).
Hugo Herbelin
2014-06-21
*
Documenting the Print Strategy command.
Pierre-Marie Pédrot
2014-03-20
*
Removing the [Require "file"] syntax.
Pierre-Marie Pédrot
2014-02-02
*
Fixing typo in reference manual from previous commit
Hugo Herbelin
2014-01-13
*
Documenting old but useful command "Print Tables".
Hugo Herbelin
2014-01-13
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Documenting the 'Printing Transparent/All Dependencies' command.
ppedrot
2012-10-30
*
Improving rendering of ldots in doc (partially done, there are too
herbelin
2012-08-11
*
Document the command Add/Remove Search Blacklist
letouzey
2012-08-03
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Documentation of last commit concerning Backtracking
letouzey
2012-03-23
*
Remove old proof-managment commands Suspend/Resume
letouzey
2012-03-23
*
Bug 2583: Update of the syntax of terms in the reference manual
pboutill
2011-09-01
*
remove old traces of SearchIsos (never ported to 7.x nor 8.x)
letouzey
2011-04-12
*
An option "Set Default Timeout n."
letouzey
2011-03-17
*
SearchAbout: who has never been annoyed by the [ ] syntax ?
letouzey
2010-11-19
*
Remove Explain* vernacs
glondu
2010-10-06
*
Remove VernacGo
glondu
2010-10-06
*
Added a section in the documentation of Vernacular commands about Set/Unset/T...
aspiwack
2010-09-23
*
Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".
herbelin
2010-06-08
*
A new command Compute foo, shortcut for Eval vm_compute in foo
letouzey
2010-06-04
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Update manual on search commands
puech
2010-03-11
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
Document Local Declare ML Module
glondu
2010-01-14
*
Documentation of the Local and Global modifiers.
herbelin
2009-10-27
*
Add doc for [Print Opaque Dependencies] and a better explanation for the
msozeau
2009-06-26
*
Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs
herbelin
2009-04-28
*
RefMan: a label defined twice
letouzey
2009-03-14
*
doc et CHANGES pour la commande Timeout
barras
2009-03-04
*
- Fixed bug #2021 (uncaught exception with injection/discriminate when
herbelin
2009-01-01
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
Document native "Declare ML Module"
glondu
2008-10-29
*
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
herbelin
2008-10-19
*
Backporting 11445 from 8.2 to trunk (negative conditions in
herbelin
2008-10-11
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
Strategy commands are now exported
barras
2008-05-22
*
refined the conversion oracle
barras
2008-05-21
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Chgts mineurs:
herbelin
2008-04-03
*
Standardisation du format des références croisées vers Figure, Section, Ch...
herbelin
2008-01-05
*
Changes in Backtrack documentation. More accurate.
courtieu
2007-09-25
*
Added the documentation for Backtrack and BackTo.
courtieu
2007-09-24
[next]