diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 03:21:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 03:21:58 +0100 |
| commit | 7e6e533b148c9d57251388e9f1646a6829d10bfb (patch) | |
| tree | f1b4f7e9c0f90128ddb8b7ccc218d0a784bd5e05 /lib/genarg.mli | |
| parent | 029854c7f0c10caf0c26b1e3d73ae011c54ac80e (diff) | |
Fixing an interpretation bug with tactics in notations. For some obscure
reason, Ltac interpretation does not allow tactics of the following
shape : let x := bla in TacGeneric tac. Hence we force genargs to be
tactics and build the resulting hole tactic from scratch.
Diffstat (limited to 'lib/genarg.mli')
0 files changed, 0 insertions, 0 deletions