diff options
| author | Arnaud Spiwack | 2014-07-29 13:19:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-29 17:16:29 +0200 |
| commit | 9e8316d8fd6a13966c21ef77d5fcba270bc9a32a (patch) | |
| tree | 99046866a67cf09557470d53e00aa9173fa87a7f /kernel/nativecode.ml | |
| parent | 52247f50fa9aed83cc4a9a714b6b8f779479fd9b (diff) | |
Untyped term in tactics: add an grammar entry to construct them.
The syntax is uconstr:term.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions