aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacentries.ml
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar 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
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Generate more user-readable tactic notation kernel names.Gravatar Pierre-Marie Pédrot2016-05-16
* 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
* AlistNsep token now accepts an arbitrary separator.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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
* Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* Generate parsing rules for ML tactics in the same order as before a7917a32.Gravatar Pierre-Marie Pédrot2016-05-02
* Useless code in Tacentries.Gravatar Pierre-Marie Pédrot2016-05-02
* Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Gravatar Hugo Herbelin2016-04-27
* A fix to #3709: ensuring extra parentheses when a tactic entry has aGravatar Hugo Herbelin2016-04-27
* Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
* Factorizing code in tactic notations.Gravatar Pierre-Marie Pédrot2016-04-25
* Documenting API.Gravatar Pierre-Marie Pédrot2016-04-25
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Disentangle tactic notation resolution from Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Factorizing the declaration of ML notation printing in Tacentries.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* 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
* Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:20:59 +0000