diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 20:50:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-04 17:33:46 +0200 |
| commit | 06ae11ea4e18766007579d47ee73b7b292a75ba4 (patch) | |
| tree | 994b8b7de3f2aa59262af2c902228a8498aeb8c3 /engine | |
| parent | 1136dde7b523047e6091d6e6decb45183e42fc21 (diff) | |
[vernac] Switch back `auto_ind_decl` to Constr.
AFAICT this tactic is always used on ground terms.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions