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
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Small doc fix : module subtyping cannot force access of opaques
letouzey
2013-04-04
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Typo in refman (fix #2962)
letouzey
2013-03-25
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
Fixing an old pecularity of "red": head betaiota redexes are now
herbelin
2013-03-21
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
Documentation of the "Local Definition" command.
ppedrot
2013-03-11
*
Added missing documentation of Set Printing Existential Instances.
herbelin
2013-02-21
*
Documenting the 'Printing Transparent/All Dependencies' command.
ppedrot
2012-10-30
*
RefMan-tac: fix a few glitches concerning the documentation of eqn:
letouzey
2012-10-23
*
Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...
gmelquio
2012-09-16
*
Some more fixes to tactic documentation.
gmelquio
2012-09-16
*
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
[next]