aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
| | | | | | | | in Relation_Operators.v and Operators_Properties.v more uniform in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 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
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
| | | | | | | | | This allow in particular to write eq instead of (@eq _) in signatures of morphisms. I dont really see how this could break existing code, no change in the stdlib was mandatory. We'll check the contribs tomorrow... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option "Unset Dependent Propositions Elimination" to protectGravatar herbelin2009-10-03
| | | | | | | | | | against the incompatibilities introduced by making "destruct" working on dependent propositions (incompatibilities come from uses of destruct in Ltac definitions such as "destruct_conjs"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 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
* Addendum to revision 12323; update Makefile.common after removal ofGravatar herbelin2009-09-11
| | | | | | | | ExternalProvers.tex in revision 12320. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
| | | | | | | | | | - Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r, Rmult_le_reg_r (mirrored variants of the existing _l lemmas); - minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs); - Rle_abs (RRle_abs); - Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 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
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
| | | | | | | | | | | | is true. E.g. "decide (eq_nat_dec n 0) with H" on H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1 returns H: n=0 |- 1 = 1 . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
| | | | | | | | | compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq (maybe an option would be better??). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 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
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
| | | | | | | | | | | | | | | The compare functions are still functions-by-tactics, but now their computational parts are completely pure (no use of lt_eq_lt_dec in nat_compare anymore), while their proofs parts are simply calls to (opaque) lemmas. This seem to improve the efficiency of sets/maps, as mentionned by T. Braibant, D. Pous and S. Lescuyer. The earlier version of nat_compare is now called nat_compare_alt, there is a proof of equivalence named nat_compare_equiv. By the way, various improvements of proofs, in particular in Pnat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
| | | | | | | | - Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
* File forgotten in commit 12171.Gravatar herbelin2009-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12173 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
| | | | | | | | | | revealed a too strict test for detection of inferable metas in Clenv. Restored tolerance for unbound names in interactive tactic use. - Moral removals of some captures of Not_found in Environ.evaluable_* since kernel is assumed to deal with existing names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
| | | | | | | | | | | | | reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
| | | | | | | | in both files. Late update of CHANGES wrt classical Tauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12084 85f007b7-540e-0410-9357-904b9bb8a0f7
* Display the content of the list instead of "<list>" when an idtacGravatar herbelin2009-04-05
| | | | | | | | | argument is a variable bound to a list (see S. Lescuyer's message on coq-club, Apr 5, 2009). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGESGravatar glondu2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12040 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"Gravatar herbelin2009-03-23
| | | | | | | | is not so robust). - Updating CHANGES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12008 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
* 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
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add -coqtoolsbyteflags and -custom to ./configure...Gravatar glondu2009-02-11
| | | | | | ...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).Gravatar herbelin2009-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11862 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
| | | | | | | | - Adding ability to use "_" in syntax for binders (as in "exists _:nat, True"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added installation of .cmi files in "make install" target of coq_makefile.Gravatar herbelin2009-01-04
| | | | | | | | Updated CHANGES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
* UpdateGravatar herbelin2009-01-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
| | | | | | | | | identity. Add notations for compatibility and support for understanding these notations in the ml files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
| | | | | | | | | | | | | - Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSet/OrderedType now includes an eq_dec, and hence become an extension of ↵Gravatar letouzey2008-12-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | DecidableType After lots of hesitations, OrderedType now requires this "eq_dec" field, which is redundant (can be deduced from "compare"), but allows the subtyping relation DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly extensions of weak sets. Of course this change introduces a last-minute incompatibility, but: - There is a clear gain in term of functionnality / simplicity. - FSets 8.2 already needs some adaptations when compared with 8.1, so it's the right time to push such incompatible changes. - Transition shouldn't be too hard: the old OrderedType still exists under the name MiniOrderedType, and functor MOT_to_OT allows to convert from one to the other. Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType (resp. OrderedType), an eq_dec on sets is now required in these interfaces and in the implementations. In pratice, it is really easy to build from equal and equal_1 and equal_2. Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun, while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M). Idem with WDecide, WProperties and WEqProperties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
* About "apply in":Gravatar herbelin2008-12-09
| | | | | | | | | | | | | | | | | | - Added "simple apply in" (cf wish 1917) + conversion and descent under conjunction + contraction of useless beta-redex in "apply in" + support for open terms. - Did not solve the "problem" that "apply in" generates a let-in which is type-checked using a kernel conversion in the opposite side of what the proof indicated (hence leading to a potential unexpected penalty at Qed time). - When applyng a sequence of lemmas, it would have been nice to allow temporary evars as intermediate steps but this was too long to implement. Smoother API in tactics.mli for assert_by/assert_as/pose_proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor improvement to commit 11619Gravatar herbelin2008-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
| | | | | | | | slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
| | | | | | | | | | revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
| | | | | | | | | | | | | | | | | | | | CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document native "Declare ML Module"Gravatar glondu2008-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11523 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
| | | | | | | | | | | - Fixed doc of assert as. - Doc of apply in + update credits. - Nettoyage partiel de Even.v en utilisant "Theorem with". - Added check that name is not in use for "generalize as". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
| | | | | | | de l'utilisation des modificateurs Global/Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11480 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
| | | | | | | | | | | | - Extension du test de réversibilité acyclique des notations dures aux notations de type abbréviation (du genre inhabited A := A). - Ajout options Local/Global à Transparent/Opaque. - Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé dependent retiré). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
| | | | | | | | SearchAbout + referring objects by their notation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
| | | | | | | | | recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES and INSTALLGravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11379 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:37:49 +0000