aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Minor fixes: Gravatar msozeau2008-04-05
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Chgts mineurs:Gravatar herbelin2008-04-03
* Typo affichage "simple apply"Gravatar herbelin2008-04-01
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* repair for commit 10612 (due to grammar order, some syntaxes weren't working) Gravatar letouzey2008-03-06
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* use loc instead of dummy_loc in the ugly intro-pattern rewrite hackGravatar letouzey2008-03-04
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* fixed pp for declarative modeGravatar corbinea2008-02-19
* Ajout de caractères unicode reconnus apr le lexerGravatar notin2008-02-18
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14