aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* Oops... forgot to commit a file related to r11561.Gravatar msozeau2008-11-09
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* allowed patternidents starting with an '_'Gravatar amahboub2008-10-31
* The lexer is changer to break former PATTERNIDENT into two tokens.Gravatar amahboub2008-10-30
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* duplicated open of PpconstrGravatar letouzey2008-10-21
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Report 11364 de 8.2 vers trunk (bugs affichage Print Module)Gravatar herbelin2008-09-05
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* - Remove some dead code in subtacGravatar msozeau2008-09-02
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* fixed indentation of subgoals for Show ScriptGravatar barras2008-07-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* Correction d'un autre bug autour de la gestion des niveaux vides deGravatar herbelin2008-07-11
* Bug résiduel du backtrack de coqide se produisant lorsque la limite deGravatar herbelin2008-07-10
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* removed unwanted linebreaks in pretty printingGravatar corbinea2008-06-19
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Fix the number parsing/printing for BigN/BigZ/BigQGravatar letouzey2008-06-10
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 21:14:35 +0000