aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2015-12-06RefMan, ch. 4: Consistent use of the terms local context and global environment.Hugo Herbelin
2015-12-06RefMan, ch. 4: Terminology constant/names.Hugo Herbelin
2015-12-06RefMan, ch. 4: Minor changes for spacing, clarity.Hugo Herbelin
2015-12-05Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Improving syntax of pat/constr introduction pattern so thatHugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-26Adding the Printing Projections options to the index.Pierre-Marie Pédrot
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-07Fixing documention of Add Printing Coercion.Hugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Reference Manual: Applying standard style recommendation about notHugo Herbelin
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Documenting matching under binders.Hugo Herbelin
2015-10-10Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-04Fix typo. (Fix bug #4355)Guillaume Melquiond
2015-10-02Fixing error messages about Hint.Hugo Herbelin
2015-10-02Improving reference manual in that auto uses simple apply rather than apply.Hugo Herbelin
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-30Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).Hugo Herbelin
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-26Documenting how to support some special unicode characters in coqdocHugo Herbelin
2015-09-26Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Hugo Herbelin
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-09-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-10typo in refman.Pierre Courtieu
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-17Remove generatable documentation files from repository. (Fix bug #4315)Guillaume Melquiond
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-07-31Fix typos in the Extraction part of the reference manual.Guillaume Melquiond
2015-07-31Fix typos in the Micromega part of the reference manual.Guillaume Melquiond
2015-07-31Improve the table of content of the reference manual.Guillaume Melquiond
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot