| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-26 | Improve tactic interpreter registration API a bit | Gaëtan Gilbert | |
| Using it feels nicer this way, with GADT details hidden inside comtactic | |||
| 2020-10-09 | [stm] move par: implementation to vernac/comTactic and stm/partac | Enrico Tassi | |
| The current implementation of par: is still in the STM, but is optional. If the STM does not take over it, it defaults to the implementation of in comTactic which is based on all: (i.e. sequential). This commit also moved the interpretation of a tactic from g_ltac to vernac/comTactic which is more appropriate. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |