diff options
| author | Pierre Boutillier | 2013-12-19 18:19:10 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2013-12-19 18:19:10 +0100 |
| commit | 5524273641556c81ce8f591861b19eae00fec27b (patch) | |
| tree | 8e1513de7386147b9cd2d724e389337c0ae10756 /kernel/nativelambda.mli | |
| parent | 7c4dee1381546347df8b473ef3986b654f03c33d (diff) | |
Bad use of Obj.magic in interpretation of TacAlias arguments.
It triggered nonsensical behaviour of list-using tactic
notation. Hopefully or not, nobody uses such notations out of
the test-suite...
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions