aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2008-04-16Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)letouzey
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-05Minor fixes: msozeau
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin
2008-04-04Quelques améliorations des intro patterns:herbelin
2008-04-03Chgts mineurs:herbelin
2008-04-01Typo affichage "simple apply"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-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-27Various fixes on typeclasses:msozeau
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-15Do a second pass on the treatment of user-given implicit arguments. Nowmsozeau
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
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-06repair for commit 10612 (due to grammar order, some syntaxes weren't working) letouzey
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-03-04use loc instead of dummy_loc in the ugly intro-pattern rewrite hackletouzey
2008-03-01Rework on rich forms of rewriteletouzey
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-19fixed pp for declarative modecorbinea
2008-02-18Ajout de caractères unicode reconnus apr le lexernotin
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2008-02-10suppression code mort oublié lors du commit 10495herbelin
2008-02-02fix the syntax "Include Type Foo"letouzey
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-30Support for substructures in classes using :> notationmsozeau
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-17fixed script printingcorbinea
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2008-01-05Correction bug #1749 (datant de l'implantation des or-patterns) +herbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-12-17Print Assumptions est pret pour la release.aspiwack
2007-12-14Correction ordre d'affichage des champs des Recordherbelin
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