aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/rewrite.ML
diff options
context:
space:
mode:
authorJosh Chen2020-08-09 18:34:58 +0200
committerJosh Chen2020-08-09 18:34:58 +0200
commit8f4ff41d24dd8fa6844312456d47cad4be6cb239 (patch)
tree05cb7780daead07c4714daa7e1fc19c940283b02 /spartan/core/rewrite.ML
parentc530305cbcafba9f66f1a55a1b5177a62f52535c (diff)
(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
Diffstat (limited to 'spartan/core/rewrite.ML')
0 files changed, 0 insertions, 0 deletions