aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-12-09About "apply in":herbelin
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-11-10Fix mixup between Record, Structure and Class by adding a new variant formsozeau
2008-11-09Oops... forgot to commit a file related to r11561.msozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-10-31allowed patternidents starting with an '_'amahboub
2008-10-30The lexer is changer to break former PATTERNIDENT into two tokens.amahboub
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-21duplicated open of Ppconstrletouzey
2008-10-20Renommage "Global Instance" en "Instance Global" pour uniformisationherbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
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-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-09-05Report 11364 de 8.2 vers trunk (bugs affichage Print Module)herbelin
2008-09-03Correct handling of implicit arguments in [Equations] definitions,msozeau
2008-09-02- Remove some dead code in subtacmsozeau
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
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-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-07-17fixed indentation of subgoals for Show Scriptbarras
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-15Autour du parsing:herbelin
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-07-10Bug résiduel du backtrack de coqide se produisant lorsque la limite deherbelin
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-06-19removed unwanted linebreaks in pretty printingcorbinea
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10Fix the number parsing/printing for BigN/BigZ/BigQletouzey
2008-06-09- Correction de la version simplifiée (filtrage sur deux sigherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 10:25:26 +0000