aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/auto_ind_decl.ml
Commit message (Expand)AuthorAge
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* About "apply in":Gravatar herbelin2008-12-09
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* * Factorizing code : context_chop was used in several files (even as chop_con...Gravatar vsiles2008-03-17
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05