diff options
| author | Pierre-Marie Pédrot | 2016-06-20 19:54:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-24 15:16:03 +0200 |
| commit | 1eea5f0081264ccb01a12f682734e8a624f83804 (patch) | |
| tree | 251df7b629e42e1c9cd2be6808b98572646f028c /kernel/nativelib.ml | |
| parent | 922ad0c1cb4a4badf4c9c2cd098285a008495519 (diff) | |
Optimization in the subst tactic.
We use simple variable substitution instead of full-power term
matching.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions