aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'Toplevel' language from extraction documentation, since it is not ↵Gravatar gmelquio2009-11-04
| | | | | | currently supported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12208 de la v8.2 (correction du bug #2126)Gravatar notin2009-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #2175Gravatar notin2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12456 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in the refmanGravatar puech2009-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of the Local and Global modifiers.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Setoid documentation.Gravatar msozeau2009-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12421 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing XML doc (COQ_XML not working as an environment variable).Gravatar herbelin2009-10-24
| | | | | | | Fixing English grammar in inversion error message (reported in bug #2164). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)Gravatar herbelin2009-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12404 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo in doc of Extraction BlacklistGravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typos.Gravatar gmelquio2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Micromega doc : psatz Z -> psatz Z 2Gravatar fbesson2009-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ltac doc: only variables are accepted as message_tokenGravatar glondu2009-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless MonoList.vGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 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
* Clarify documentation of ltac repeatGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12335 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
| | | | | | | | | | | | | | interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add doc of [Context] vernacular.Gravatar msozeau2009-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Gappa from the external provers supported by the dp plugin. Tactic ↵Gravatar gmelquio2009-09-11
| | | | | | gappa has been supported for some time in an external package. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchGravatar msozeau2009-09-08
| | | | | | | by Chris Casinghino). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor spelling errorGravatar glondu2009-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12300 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵Gravatar fbesson2009-08-25
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
| | | | | | | flags of manual implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12200 (bug #2125)Gravatar notin2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Ian Lynagh's documentation fixes patch (see bug #2112)Gravatar herbelin2009-06-06
| | | | | | | | [copy of revision 12164 from branch v8.2] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12165 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
| | | | | | | | | | | | | (bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting 12112 from v8.2 branch to trunk (fixing documentation bugsGravatar herbelin2009-04-28
| | | | | | | | #2099 in ConstructiveEpsilon.v and #2100 on Global Opaque). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document new quote constructionGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12039 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
* RefMan: a label defined twiceGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11978 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep: remove references to obsolete .zi and Require Implementation stuffGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc et CHANGES pour la commande TimeoutGravatar barras2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11962 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
* Modification du style du manuel de référenceGravatar notin2009-02-11
| | | | | | (cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
| | | | | | | | | few hevea warning (failure to put a vector on an expression in Classes.tex, failure to support multirow in RecTutorial.tex). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
| | | | | | | | | | - Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
| | | | | | | scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
| | | | | | | | from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added some missing statements for proof folding and correctedGravatar vgross2009-01-20
| | | | | | | | the reference manual accordingly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added proof folding into CoqIde. See RefMan for using it.Gravatar vgross2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11814 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 03:41:36 +0000