aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Added option "Unset Dependent Propositions Elimination" to protectGravatar herbelin2009-10-03
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Addendum to revision 12323; update Makefile.common after removal ofGravatar herbelin2009-09-11
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* Removed Gappa from the external provers supported by the dp plugin. Tactic ga...Gravatar gmelquio2009-09-11
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchGravatar msozeau2009-09-08
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* File forgotten in commit 12171.Gravatar herbelin2009-06-07
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
* Display the content of the list instead of "<list>" when an idtacGravatar herbelin2009-04-05
* Update CHANGESGravatar glondu2009-03-30
* - Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"Gravatar herbelin2009-03-23
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* doc et CHANGES pour la commande TimeoutGravatar barras2009-03-04
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* Add -coqtoolsbyteflags and -custom to ./configure...Gravatar glondu2009-02-11
* Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).Gravatar herbelin2009-01-27
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Added installation of .cmi files in "make install" target of coq_makefile.Gravatar herbelin2009-01-04
* UpdateGravatar herbelin2009-01-01
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* Minor improvement to commit 11619Gravatar herbelin2008-11-23
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 16:51:46 +0000