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