diff options
| author | Pierre-Marie Pédrot | 2015-12-22 15:39:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-28 02:33:43 +0100 |
| commit | 9af1d5ae4dbed8557b5c715a65f2742c57641f52 (patch) | |
| tree | dac7e73c397edb30ffdd4e076d4efe792a8464bc /plugins/syntax/string_syntax.ml | |
| parent | cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 (diff) | |
Implementing non-focussed generic arguments.
Kind of enhances the situation of bug #4409. Now arguments can be interpreted
globally or focussedly in a dynamic fashion because the interpretation function
returns a Ftactic.t. The bug is not fixed yet because we should tweak the
interpretation of tactic arguments.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions