aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Renaming binders into binderlists in egramcoq.ml.Gravatar Hugo Herbelin2018-02-20
* Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Gravatar Hugo Herbelin2018-02-20
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Releasing level "11" of "pattern".Gravatar Hugo Herbelin2017-11-27
* Fixing associativity registered for level 10.Gravatar Hugo Herbelin2017-11-27
* Merge PR #6167: Fixing factorization of recursive notations with an atomic se...Gravatar Maxime Dénès2017-11-23
|\
| * Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
* | [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/
* Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Gravatar Hugo Herbelin2017-09-25
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* G_prim: the bigint entry keeps numbers in raw stringsGravatar Pierre Letouzey2017-06-14
* Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [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
|/
* Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\
* | Fix an error-prone error API.Gravatar Pierre-Marie Pédrot2016-09-21
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
* Making the grammar command extend API purely functional.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the constr empty entry registering to the state-based API.Gravatar Pierre-Marie Pédrot2016-05-11
* Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
* Further tidying of the constr extension code.Gravatar Pierre-Marie Pédrot2016-05-10
* Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-05-10
* Purer implementation of empty level registering in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
* Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* | Abstracting away the Summary-synchronized grammar-modifying commands.Gravatar Pierre-Marie Pédrot2016-03-31
* | Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
* | Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Gravatar Pierre-Marie Pédrot2016-03-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 09:45:20 +0000