aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/depends.ml
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-12-09About "apply in":herbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-08Autre oubli de la révision 10904herbelin
2008-04-14oubli sur 10790herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
2008-03-01Rework on rich forms of rewriteletouzey
2008-02-25Forgotten file in previous commitlmamane