diff options
| author | Hugo Herbelin | 2014-09-10 12:29:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-10 12:31:22 +0200 |
| commit | dcac2e58843c53137e740fc1bf324ddc16932223 (patch) | |
| tree | 586c8daf8f642f3e0418e02edbb1be31966d3232 /kernel/inductive.ml | |
| parent | 2bb166e09d829c3d70b99d1cb9c74511e47f517e (diff) | |
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions