aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/context_tactical.ML (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-211-5/+28
| | | | better. 2. Changed most tactics to context tactics.
* Checkpoint. THIS BUILD WILL FAILJosh Chen2020-07-161-0/+129