index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
tacentries.ml
Commit message (
Expand
)
Author
Age
*
Adding the Print Ltac Signature command.
Pierre-Marie Pédrot
2016-06-05
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Generate more user-readable tactic notation kernel names.
Pierre-Marie Pédrot
2016-05-16
*
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-11
*
AlistNsep token now accepts an arbitrary separator.
Pierre-Marie Pédrot
2016-05-10
*
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
*
Pass user symbol to tactic notation printers.
Pierre-Marie Pédrot
2016-05-08
*
Generate parsing rules for ML tactics in the same order as before a7917a32.
Pierre-Marie Pédrot
2016-05-02
*
Useless code in Tacentries.
Pierre-Marie Pédrot
2016-05-02
*
Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"
Hugo Herbelin
2016-04-27
*
A fix to #3709: ensuring extra parentheses when a tactic entry has a
Hugo Herbelin
2016-04-27
*
Merging the ML tactic notation and plain Tactic Notation mechanisms.
Pierre-Marie Pédrot
2016-04-25
*
Factorizing code in tactic notations.
Pierre-Marie Pédrot
2016-04-25
*
Documenting API.
Pierre-Marie Pédrot
2016-04-25
*
Remove dead registering code in Pcoq.
Pierre-Marie Pédrot
2016-04-24
*
Disentangle tactic notation resolution from Pcoq.
Pierre-Marie Pédrot
2016-04-24
*
Higher-level API for tactic notations.
Pierre-Marie Pédrot
2016-04-24
*
Factorizing the declaration of ML notation printing in Tacentries.
Pierre-Marie Pédrot
2016-04-24
*
Moving and enhancing the grammar_tactic_prod_item_expr type.
Pierre-Marie Pédrot
2016-04-14
*
Getting rid of the "_mods" parsing entry.
Pierre-Marie Pédrot
2016-04-01
*
Moving the code handling tactic notations to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
Moving the Tactic Notation entry parser from Pcoq to Tacentries.
Pierre-Marie Pédrot
2016-03-31
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Hugo Herbelin