aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2012-03-19RefMan: Environment variables description updatepboutill
2012-02-29RefMan update about match syntax.pboutill
2012-02-18Document the [unify] tactic.msozeau
2012-02-07Documentation for Grab Existential Variables.aspiwack
2012-02-01Corrected a careless cut-and-paste in Gallina description which dated back to...ppedrot
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
2012-01-19Added the btauto tactic to the documentation.ppedrot
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-12Proof using ...gareuselesinge
2011-12-06Documentation of Arguments + implicitsgareuselesinge
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
2011-12-06Documentation for Arguments + simplgareuselesinge
2011-12-04Fixing bugs in doc about when "with" is needed or not to give bindingsherbelin
2011-11-29Documentation of appcontextletouzey
2011-11-28doc: two minor fixes to make my latex happyletouzey
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-10-18Extraction.tex: typo in an Extract Inductive example (fix #2625)letouzey
2011-10-07A new tactic is_var to check whether a term is a goal/section variableletouzey
2011-10-07Remove 'status' of Program and explain the :> better, as well as referencing ...msozeau
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
2011-09-17doc/refman/Extraction.tex: no need to actually build euclid.mlletouzey
2011-09-05Remove code concerning the obsolete Set/Unset Undoletouzey
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-09-01Several bug reports came from confusions between generalize and set.pboutill
2011-09-01Bug 2583: Update of the syntax of terms in the reference manualpboutill
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-07-07coq_makefile documentation in Refman and -hpboutill
2011-06-29update of Micromega docfbesson
2011-06-16refman nsatzpottier
2011-04-28Adding "Tactic Notation" in doc index.herbelin
2011-04-15Documentation typo.gmelquio
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
2011-04-08@ in index of refman (last request of bug 2494)pboutill
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-17An option "Set Default Timeout n."letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 12:07:01 +0000