index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
parsing
/
egramcoq.ml
Age
Commit message (
Expand
)
Author
2018-05-27
[api] [parsing] Move Egram* to `vernac/`
Emilio Jesus Gallego Arias
2018-03-09
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-20
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
Renaming binders into binderlists in egramcoq.ml.
Hugo Herbelin
2018-02-20
Introducing an intermediary type "constr_prod_entry_key" for grammar producti...
Hugo Herbelin
2018-02-20
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Hugo Herbelin
2018-02-17
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2017-11-27
Releasing level "11" of "pattern".
Hugo Herbelin
2017-11-27
Fixing associativity registered for level 10.
Hugo Herbelin
2017-11-23
Merge PR #6167: Fixing factorization of recursive notations with an atomic se...
Maxime Dénès
2017-11-20
Fixing factorization of recursive notations in the case of an atomic separator.
Hugo Herbelin
2017-11-19
[parser] Remove unnecessary statically initialized hook.
Emilio Jesus Gallego Arias
2017-09-25
Fixing a little parsing bug with level 90 introduced in 3e70ea9c.
Hugo Herbelin
2017-08-29
A new step of restructuration of notations.
Hugo Herbelin
2017-08-29
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-07-26
Adding support for recursive notations of the form "x , .. , y , z".
Hugo Herbelin
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-14
G_prim: the bigint entry keeps numbers in raw strings
Pierre Letouzey
2017-06-14
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
Pierre Letouzey
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-03-24
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2016-09-23
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-21
Fix an error-prone error API.
Pierre-Marie Pédrot
2016-09-16
Addressing OCaml compilation warnings.
Hugo Herbelin
2016-08-19
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-07
Removing the use to Egramcoq.recover_constr_grammar.
Pierre-Marie Pédrot
2016-05-11
Making the grammar command extend API purely functional.
Pierre-Marie Pédrot
2016-05-11
Moving the constr empty entry registering to the state-based API.
Pierre-Marie Pédrot
2016-05-11
Turning the grammar extend command API into a state-passing one.
Pierre-Marie Pédrot
2016-05-11
Moving the grammar summary to Pcoq.
Pierre-Marie Pédrot
2016-05-10
Further tidying of the constr extension code.
Pierre-Marie Pédrot
2016-05-10
Type-safe constr notations.
Pierre-Marie Pédrot
2016-05-10
Purer implementation of empty level registering in Pcoq.
Pierre-Marie Pédrot
2016-05-10
Hardening the obsolete unsafe_grammar_statement API.
Pierre-Marie Pédrot
2016-05-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-03-31
Moving the code handling tactic notations to Tacentries.
Pierre-Marie Pédrot
2016-03-31
Abstracting away the Summary-synchronized grammar-modifying commands.
Pierre-Marie Pédrot
[next]