aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
AgeCommit message (Expand)Author
2008-09-07Add the ability to declare [Hint Extern]'s with no pattern.msozeau
2008-09-07Fixes in typeclasses resolution. Avoid reducing instances types beforemsozeau
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-06-29Correction bug "parser" suite changement syntaxeherbelin
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-06-12Correction parser révélé par test-suiteherbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-08Autre oubli de la révision 10904herbelin
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-14oubli sur 10790herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Correction problème de compil (blast.ml)herbelin
2008-04-04Quelques améliorations des intro patterns:herbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-04-01Ajout "simple apply" et "simple eapply" pour apply sans unfoldherbelin
2008-03-30Suite commit 10730: MAJ xlate.mlherbelin
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-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-03-01Rework on rich forms of rewriteletouzey
2008-02-25Forgotten file in previous commitlmamane
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-07Completion of 10427...herbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-09Nettoyage de Print Assumptions :aspiwack
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-10-01Complément nécessaire aux révisions 10156 et 10157herbelin
2007-09-28Modification of the Scheme command.vsiles
2007-08-30Oubli dans commit 10102...herbelin