aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* g_tactics : remove opt_bindings (2-line dead code)Gravatar Pierre Letouzey2016-06-01
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* 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
* 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
* 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
* 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
* | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing a mispelling coma -> comma."Gravatar Hugo Herbelin2016-04-27
* | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-04-27
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-04-25
* | Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * A fix to #4666 (Exc_located capsule added by camlp5 overwritingGravatar Hugo Herbelin2016-04-12
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* | | Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* | | 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
* | | Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* | | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Moving the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Allowing generalized rules in typed symbols.Gravatar Pierre-Marie Pédrot2016-03-19
* | | Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 09:03:19 +0000