diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 13:26:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 14:27:18 +0200 |
| commit | a622696bbe5c6752e49dabb4d3740acf113080ee (patch) | |
| tree | c556bcef3405b85cb2ae858752fa37f61a5883ae /parsing/g_tactic.ml4 | |
| parent | b976aa1e49579b7b50cfb140cbac8cb6f4c881a7 (diff) | |
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Diffstat (limited to 'parsing/g_tactic.ml4')
0 files changed, 0 insertions, 0 deletions