aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/faq
Commit message (Collapse)AuthorAge
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
* update Proof General URLGravatar Paul Steckler2016-08-23
|
* 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
| | | | | | The .png was ugly (less than 400px wide) and did not match the content of the .fig file (e.g. presence of '$'). To improve things a bit, text is now rendered by latex.
* 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
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* 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
| | | | | | | | | | | I'm not quite sure why, but I'm pretty sure it's not. Rather, in "allowing for foo" and "allowing to foo", "foo" modifies the sense in which someting is allowed, rather than it being "foo" that's allowed. "Allowing fooing" generally works, though it can sound a bit awkward. "Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always acceptable, in-as-much as it's ok to use "one". I haven't touched the older instances of it in the CHANGES file.
* 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
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixup r15251 second timeGravatar pboutill2012-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed the quasi-useless gtk2rc file and the documentation that went with ↵Gravatar ppedrot2012-04-27
| | | | | | it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
* - changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵Gravatar notin2012-02-20
| | | | | | | | available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc: two minor fixes to make my latex happyGravatar letouzey2011-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14733 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating some links in the FAQGravatar herbelin2011-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Jean-Baptiste Rouquier's FAQ update proposed on coqdev aboutGravatar herbelin2011-09-24
| | | | | | using unicode in X11. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Example of a simple ML tactic (Hello world).Gravatar fkirchne2010-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).Gravatar herbelin2010-12-04
| | | | | | It is in section "My goal is ..., how can I prove it?" of the FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
| | | | | | user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj de la faq: correction de l'exemple field qui compilait plus en 8.2, ↵Gravatar jnarboux2009-02-17
| | | | | | correction de quelques typos, maj des <<related tools>>, suppression des questions sans reponse git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11931 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous CoqideGravatar notin2008-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la question no 172 de la FAQ (cf bug #1755)Gravatar notin2007-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
| | | | | | | | Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1635Gravatar notin2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo faqGravatar herbelin2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation de la FAQGravatar notin2007-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction typo règle réduction du fix chapitre CCIGravatar herbelin2006-12-08
| | | | | | | Maj mode emacs coqide dans faq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
* add a comment about Show Existentials and a question about case_eq Gravatar jnarboux2006-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite actualisation FAQGravatar herbelin2006-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:22:45 +0000