aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* - 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
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Document native "Declare ML Module"Gravatar glondu2008-10-29
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Update CHANGES and INSTALLGravatar glondu2008-09-07
* Renaming parser -> coq-parserGravatar glondu2008-08-18
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Add -browser option to configure scriptGravatar glondu2008-07-27
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* MAJ fichiers spécifiques trunkGravatar herbelin2008-06-22
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* MAJ diversesGravatar herbelin2008-06-11
* Documentation de "instantiate".Gravatar glondu2008-06-09
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* add tiny change to coqideGravatar jnarboux2008-06-07
* One (last?) more update of CHANGES.Gravatar letouzey2008-06-05
* more updates of CHANGESGravatar letouzey2008-06-04
* Some updates of CHANGES (to be continued...)Gravatar letouzey2008-06-03
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
* update changes related to coqideGravatar jnarboux2008-05-27
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 13:12:56 +0000