aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/faq
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove generatable documentation files from repository. (Fix bug #4315)Gravatar Guillaume Melquiond2015-08-17
* Avoid suggesting elim and decompose in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Remove some output of Qed in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Improve the FAQ a bit.Gravatar Guillaume Melquiond2015-07-29
* Reset a dangling proof in the FAQ.Gravatar Guillaume Melquiond2015-07-28
* Regenerate the axiom figure of the FAQ.Gravatar Guillaume Melquiond2015-07-26
* Remove obsolete question about eta-conversion.Gravatar Guillaume Melquiond2015-07-26
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* FAQ: fix some broken urlsGravatar Pierre Letouzey2014-11-27
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
* Completing text of the question on conservativity of CIC over CC (bug #2697).Gravatar Hugo Herbelin2014-04-05
* Fix Bug 3131 + Really drop mentions of info in refman.Gravatar Pierre Boutillier2014-04-02
* Updating version numbers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* Fixup r15251 second timeGravatar pboutill2012-05-03
* Removed the quasi-useless gtk2rc file and the documentation that went with it...Gravatar ppedrot2012-04-27
* - changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...Gravatar notin2012-02-20
* doc: two minor fixes to make my latex happyGravatar letouzey2011-11-28
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
* Updating some links in the FAQGravatar herbelin2011-10-01
* Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutGravatar herbelin2011-09-24
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
* Example of a simple ML tactic (Hello world).Gravatar fkirchne2010-12-09
* Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).Gravatar herbelin2010-12-04
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...Gravatar jnarboux2009-02-17
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous CoqideGravatar notin2008-01-07
* Modification de la question no 172 de la FAQ (cf bug #1755)Gravatar notin2007-12-11
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Correction du bug #1635Gravatar notin2007-08-13
* typo faqGravatar herbelin2007-06-19
* Compilation de la FAQGravatar notin2007-02-18
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
* Correction typo règle réduction du fix chapitre CCIGravatar herbelin2006-12-08
* add a comment about Show Existentials and a question about case_eq Gravatar jnarboux2006-12-01
* Petite actualisation FAQGravatar herbelin2006-03-31
* r8637@thot: notin | 2006-03-14 16:00:49 +0100Gravatar notin2006-03-14
* Mise à jour des Makefile, ajout licences, corrections mineures suite àGravatar herbelin2006-02-23