diff options
| author | Hugo Herbelin | 2018-04-19 14:26:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-11 14:08:01 +0200 |
| commit | 8d1a5297d55eb0cd02695c81f6dea7aef6f62d31 (patch) | |
| tree | 426fc4eb9ef3d8de8960bddba19a4c5e2fcee251 /kernel/typeops.ml | |
| parent | 053193926ea1397c400355a8d253ec9ba36a5731 (diff) | |
Made names of existential variables interpretable as Ltac variables.
This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.
Moreover, with that, we can for instance do:
Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions