diff options
| author | Matthieu Sozeau | 2014-12-10 18:17:39 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-12-10 18:18:56 +0100 |
| commit | c938cb8e85f741ce697e7486d35c27c1aa31fe7a (patch) | |
| tree | fc0c9d069685674449d3ad2f0ff090ac933bd299 /plugins/syntax/string_syntax.ml | |
| parent | d8aa8ce556945cba1d3c08c97f8db78d42796a04 (diff) | |
Fix dummy argument use in guess_elim: there are some cases where X_ind
is not defined while X_rect is, for example in HoTT/Coq.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions