aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacenv.ml
Commit message (Expand)AuthorAge
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar 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
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21