aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/tacextend.mlp
Commit message (Expand)AuthorAge
* TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2016-11-03
|\
| * Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.Gravatar Pierre-Marie Pédrot2016-10-30
* | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
|/
* restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Gravatar Pierre Letouzey2016-07-26
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
* Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01