index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
...
*
Beautify tactic documentation a bit more.
gmelquio
2012-09-16
*
Remove superfluous spaces and commas in tactic documentation.
gmelquio
2012-09-16
*
Fix index generation for the pdf document.
gmelquio
2012-09-16
*
Fix failure to compile doc/stdlib/Library.tex.
gmelquio
2012-09-15
*
Port rewrites of tactic documentation from branch 8.4.
gmelquio
2012-09-15
*
Obsolete syntax in documentation of Solve Obligation commands.
ppedrot
2012-09-05
*
Add option Set/Unset Extraction Conservative Types.
aspiwack
2012-08-24
*
Remove a script unused since 2006 (cf commit r8626)
letouzey
2012-08-23
*
Extraction: document Separate Extraction and KeepSingleton
letouzey
2012-08-23
*
Improving rendering of ldots in doc (partially done, there are too
herbelin
2012-08-11
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Improving rendering of ...-separated lists and sequences in reference
herbelin
2012-08-11
*
Updating version numbers.
herbelin
2012-08-08
*
Documenting eta-conversion.
herbelin
2012-08-08
*
More standard layout for \lambda in chapter CIC.
herbelin
2012-08-08
*
Typo in r15654
herbelin
2012-08-07
*
Updating credits for final 8.4
herbelin
2012-08-07
*
Document the command Add/Remove Search Blacklist
letouzey
2012-08-03
*
documentation of bullets (forward port from v8.4).
courtieu
2012-07-25
*
Vector equalities first stuff
pboutill
2012-07-20
*
isolate instances about Permutation and PermutationA which may slow rewrite
letouzey
2012-07-10
*
The tactic remember now accepts a final eqn:H option (grant wish #2489)
letouzey
2012-07-09
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Legacy Ring and Legacy Field migrated to contribs
letouzey
2012-07-05
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
make sure that documentation compilation works after adding files for
bertot
2012-06-12
*
place all files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29
*
Fixed #2789.
ppedrot
2012-05-25
*
Addedum to documentation of bullets: I now use the dedicated coq_example
aspiwack
2012-05-10
*
Documentation for Unfocused, braces and bullets.
aspiwack
2012-05-10
*
Rephrasing section on Sorts in CIC chapter, accordingly to discussions
herbelin
2012-05-08
*
Ref. man., ch. CIC: clarifying the redundancy coming from having both
herbelin
2012-05-08
*
Fixup r15251 second time
pboutill
2012-05-03
*
Removed the quasi-useless gtk2rc file and the documentation that went with it...
ppedrot
2012-04-27
*
MSetRBT : implementation of MSets via Red-Black trees
letouzey
2012-04-13
*
Uniformisation in the documentation: remove the use of 'coinductive' in
aspiwack
2012-04-13
*
Documentation of records defined with the keywords Inductive and
aspiwack
2012-04-13
*
Restores pdf bookmarks in the reference manual.
aspiwack
2012-04-13
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
Slight change in the semantics of arguments scopes: scopes can no
herbelin
2012-03-26
*
Documentation of last commit concerning Backtracking
letouzey
2012-03-23
*
Remove old proof-managment commands Suspend/Resume
letouzey
2012-03-23
*
RefMan: Environment variables description update
pboutill
2012-03-19
*
RefMan update about match syntax.
pboutill
2012-02-29
*
- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...
notin
2012-02-20
*
Document the [unify] tactic.
msozeau
2012-02-18
*
Documentation for Grab Existential Variables.
aspiwack
2012-02-07
*
Corrected a careless cut-and-paste in Gallina description which dated back to...
ppedrot
2012-02-01
*
Improved synchronisation of stdlib index page with current library state.
herbelin
2012-02-01
[prev]
[next]