aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
Commit message (Expand)AuthorAge
* Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\
| * Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ | |/ |/|
* | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
* | Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
| * Rename release_lexer_state to the more descriptive get_lexer_state.Gravatar Jim Fehrle2018-02-22
* | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
|/
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Remove pidentref grammar entry.Gravatar Gaëtan Gilbert2017-11-20
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Gravatar Maxime Dénès2017-09-15
|\
| * Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
| * don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| * Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
|/
* Silence the CAMLP5 warnings on command line.Gravatar Pierre-Marie Pédrot2016-09-02
* Remove lexing of ordinal notations.Gravatar Maxime Dénès2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* The grammar_extend function now registers unsynchronized extensions.Gravatar Pierre-Marie Pédrot2016-05-11
* 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
* Delimiting the use of unsafe code in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
* Overlooked use of Gram instead of G module in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
* Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-05-10
* AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
* Simpler data structure for Arules token.Gravatar Pierre-Marie Pédrot2016-05-10
* Purer implementation of empty level registering in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-05-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 04:03:53 +0000