diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-24 13:52:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-24 15:16:03 +0200 |
| commit | f4f08411e85185cb03ea0ee0cb42c59988015e65 (patch) | |
| tree | 2832b87b02e05114aec2b8ce888448249d0aee76 /tactics/hipattern.ml | |
| parent | e5446e385ba283f3c4cde83e0fc14987e500778a (diff) | |
Optmimize the subst tactic.
Take advantage that the provided term is always a variable in Equality.is_eq_x.
Diffstat (limited to 'tactics/hipattern.ml')
0 files changed, 0 insertions, 0 deletions