diff options
| author | Pierre-Marie Pédrot | 2017-08-18 17:59:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 14:47:47 +0200 |
| commit | 0232b0de849998d3394a4e6a2ab6232a75897610 (patch) | |
| tree | 7c7d440f32775a1b394fff638abe78bb7e77a832 /tests | |
| parent | 0b2c0e58b45b2e78f8ad65ddbc7254e1fd9d07eb (diff) | |
Use references in reduction tactics.
We dynamically check that the provided references are indeed evaluable
ones, instead of ensuring this at internalization time.
Diffstat (limited to 'tests')
0 files changed, 0 insertions, 0 deletions