aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tauto.ml
Commit message (Expand)AuthorAge
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Do not generate generic arguments for data which only requires toplevel values.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.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
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21