Leonardo de Moura
603bbe5987
fix(*): gcc 7 linking errors
2017-05-31 16:35:09 -07:00
Leonardo de Moura
36c7d46c34
feat(library/tactic): add options trace.rewrite and trace.kabstract for debugging rewrite tactic
...
See #1480
@semorrison We can now use the following commands to trace the rewrite
tactic
```lean
set_option trace.rewrite true
set_option trace.kabstract true
```
When these options are used, Lean will pretty print the subterm selected
by the rewrite tactic. That is, the subterm that will be rewritten.
This option may help you diagnose what is going on.
2017-03-27 18:18:20 -07:00
Daniel Selsam
cddf5f081d
fix(library/tactic/kabstract.cpp): only use replace_fn cache if replacing all occs
2017-03-15 19:40:52 -07:00
Sebastian Ullrich
4d41b03168
chore(frontends/lean,library/tactic): remove old tactic_state functions
2017-02-17 15:41:58 +01:00
Leonardo de Moura
3ced85d399
feat(library/init/meta/tactic): add kdepends_on tactic
2017-02-14 10:33:28 -08:00
Gabriel Ebner
a26e2c9108
feat(library/module): intermediary data structure for environment modifications
2016-12-20 10:15:19 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
e6fbbbbc2d
feat(util/rb_map): add unsigned_map
2016-10-03 16:26:58 -07:00
Leonardo de Moura
a20abd61e8
feat(library/tactic): implement rewrite and kabstract using occurrences object
2016-07-18 10:10:37 -04:00
Leonardo de Moura
579f643d1d
refactor(library): move kabstract to tactic folder
2016-07-18 09:57:02 -04:00
