aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* /home/pirbo/.coqrc* are read againGravatar pboutill2011-11-21
* -user option removalGravatar pboutill2011-11-21
* coqrc in the right XDG_CONFIG_HOME/coq folderGravatar pboutill2011-11-20
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
* Extraction.tex: typo in an Extract Inductive example (fix #2625)Gravatar letouzey2011-10-18
* mainbiblio.bib : get rid of merge marker from failed mergeGravatar letouzey2011-10-09
* A new tactic is_var to check whether a term is a goal/section variableGravatar letouzey2011-10-07
* Remove 'status' of Program and explain the :> better, as well as referencing ...Gravatar msozeau2011-10-07
* Updating some links in the FAQGravatar herbelin2011-10-01
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutGravatar herbelin2011-09-24
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23
* doc/refman/Extraction.tex: no need to actually build euclid.mlGravatar letouzey2011-09-17
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
* Several bug reports came from confusions between generalize and set.Gravatar pboutill2011-09-01
* Bug 2583: Update of the syntax of terms in the reference manualGravatar pboutill2011-09-01
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
* coq_makefile documentation in Refman and -hGravatar pboutill2011-07-07
* doc/stdlib: Update the list of ZArith filesGravatar letouzey2011-07-04
* update of Micromega docGravatar fbesson2011-06-29
* refman nsatzGravatar pottier2011-06-16
* update of the file list in doc/stdlibGravatar letouzey2011-05-06
* Adding "Tactic Notation" in doc index.Gravatar herbelin2011-04-28
* Documentation typo.Gravatar gmelquio2011-04-15
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
* remove old traces of SearchIsos (never ported to 7.x nor 8.x)Gravatar letouzey2011-04-12
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* Restore documentation of library String which was removed in 2007 (r10049)Gravatar herbelin2011-03-05
* Remove obsolete TheoryListGravatar glondu2011-02-10
* Fix formatting issue in refmanGravatar glondu2011-01-12
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Precision in documentation of "decide equality"Gravatar glondu2010-12-24
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* More precise documentation for instantiateGravatar glondu2010-12-23
* Example of a simple ML tactic (Hello world).Gravatar fkirchne2010-12-09
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).Gravatar herbelin2010-12-04
* Documentation for tactic constr_eqGravatar glondu2010-12-02
* Add tactic has_evar (#2433)Gravatar glondu2010-12-02
* Add tactic is_evar (Closes: #2433)Gravatar glondu2010-12-02
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 03:52:23 +0000