diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-18 02:50:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-20 14:49:47 +0200 |
| commit | e705ae9d343c67212ce238899d21059ce93ee3e5 (patch) | |
| tree | 33eb5575b2da7275fdb13295243ef045afab3375 /theories/Numbers | |
| parent | f79e9db4922f649d08153f09526d5c1c60a7e45c (diff) | |
Tentative to add constr-using primitive tactics without grammar rules.
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
Diffstat (limited to 'theories/Numbers')
0 files changed, 0 insertions, 0 deletions