aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
...
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| * Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\ \
| | | * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | | * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | | * Remove unused constructorsGravatar Gaetan Gilbert2017-04-27
| | | * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | | * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |/ | |/|
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
* | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
|/ /
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \
| | * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
| |/ |/|
* | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \
* | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| * | Applying same convention as in Definition for parsing type in a let in.Gravatar Hugo Herbelin2017-03-24
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ /
| * Supporting arbitrary binders in record fields, including e.g. patterns.Gravatar Hugo Herbelin2017-03-23
| * Removing a redundant line in the syntax of record fields.Gravatar Hugo Herbelin2017-03-23
| * Factorizing/unifying code in dealing with binders.Gravatar Hugo Herbelin2017-03-23
| * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
* | [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [safe-string] parsing/cLexerGravatar Emilio Jesus Gallego Arias2017-03-14
| * don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\|
| * Fixing lexing of strings in comments for beautifier.Gravatar Hugo Herbelin2016-12-02
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix #5174: Underinformative syntax error messages in the new arguments syntaxGravatar Maxime Dénès2016-11-30
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 05:19:59 +0000