aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-10-29Document native "Declare ML Module"glondu
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-20Renommage "Global Instance" en "Instance Global" pour uniformisationherbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-09-11Add enough information to correctly globalize recursive calls in inductive andmsozeau
2008-09-07Update CHANGES and INSTALLglondu
2008-08-18Renaming parser -> coq-parserglondu
2008-08-04Évolutions diverses et variées.herbelin
2008-07-27Add -browser option to configure scriptglondu
2008-07-23Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theherbelin
2008-07-17- Suppression de Rstar/Newman peu utilisables comme biblio (encodageherbelin
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-22MAJ fichiers spécifiques trunkherbelin
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-11MAJ diversesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:24:21 +0000