index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2015-12-03
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-02
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Hugo Herbelin
2015-11-29
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
Adding the Printing Projections options to the index.
Pierre-Marie Pédrot
2015-11-10
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-07
Adding an amazing property of Prop.
Hugo Herbelin
2015-11-07
Fixing documention of Add Printing Coercion.
Hugo Herbelin
2015-11-05
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-04
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-10-19
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-18
Reference Manual: Applying standard style recommendation about not
Hugo Herbelin
2015-10-15
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-14
Fix some typos.
Guillaume Melquiond
2015-10-13
Fix some typos.
Guillaume Melquiond
2015-10-12
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-11
Documenting matching under binders.
Hugo Herbelin
2015-10-10
Fix a few latex errors in documentation of Proof Using (e.g. \tt*).
Guillaume Melquiond
2015-10-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-08
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-06
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-04
Fix typo. (Fix bug #4355)
Guillaume Melquiond
2015-10-02
Mark the Coq.Compat files for documentation. (Fix bug #4353)
Guillaume Melquiond
2015-10-02
Fixing error messages about Hint.
Hugo Herbelin
2015-10-02
Improving reference manual in that auto uses simple apply rather than apply.
Hugo Herbelin
2015-10-02
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-30
Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).
Hugo Herbelin
2015-09-28
Make -load-vernac-object respect the loadpath.
Guillaume Melquiond
2015-09-26
Documenting how to support some special unicode characters in coqdoc
Hugo Herbelin
2015-09-26
Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.
Hugo Herbelin
2015-09-25
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
The -require option now accepts a logical path instead of a physical one.
Pierre-Marie Pédrot
2015-09-25
Updating the documentation and the toolchain w.r.t. the change in -compile.
Pierre-Marie Pédrot
2015-09-21
Fixing tutorial.
Pierre-Marie Pédrot
2015-09-13
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-10
typo in refman.
Pierre Courtieu
2015-09-08
Documenting the new behaviour of the Shrink Obligations flag.
Pierre-Marie Pédrot
2015-08-22
Documenting the Shrink Abstract option.
Pierre-Marie Pédrot
2015-08-22
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-17
Remove generatable documentation files from repository. (Fix bug #4315)
Guillaume Melquiond
2015-08-05
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-02
Granting Jason's request for an ad hoc compatibility option on
Hugo Herbelin
2015-07-31
Fix typos in the Extraction part of the reference manual.
Guillaume Melquiond
2015-07-31
Fix typos in the Micromega part of the reference manual.
Guillaume Melquiond
2015-07-31
Improve the table of content of the reference manual.
Guillaume Melquiond
2015-07-31
Remove some outdated files and fix permissions.
Guillaume Melquiond
2015-07-30
Avoid suggesting elim and decompose in the FAQ.
Guillaume Melquiond
2015-07-30
Remove some output of Qed in the FAQ.
Guillaume Melquiond
2015-07-30
Fix some broken Coq scripts in the documentation.
Guillaume Melquiond
[next]