| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the use of Tactic_option from Obligations to G_obligations. | Pierre-Marie Pédrot | |
| 2016-03-17 | Removing the special status of generic arguments defined by Coq itself. | Pierre-Marie Pédrot | |
| This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |