diff options
| author | Josh Chen | 2021-06-23 16:26:23 +0100 |
|---|---|---|
| committer | Josh Chen | 2021-06-23 16:26:23 +0100 |
| commit | 0085798a86a35e2430a97289e894724f688db435 (patch) | |
| tree | db1662a5805917c6627963578f074dc226b4b06a /mltt/core/types.ML | |
| parent | 1928649fd490d50d1e05fef6cbb22ca38d81cbe5 (diff) | |
1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker
Diffstat (limited to 'mltt/core/types.ML')
| -rw-r--r-- | mltt/core/types.ML | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mltt/core/types.ML b/mltt/core/types.ML index 5e0d484..d0b1137 100644 --- a/mltt/core/types.ML +++ b/mltt/core/types.ML @@ -83,9 +83,9 @@ fun check_infer_step facts i (ctxt, st) = val ctxt' = ctxt (*TODO: Use this to store already-derived typing judgments*) in TACTIC_CONTEXT ctxt' ( - (NO_CONTEXT_TACTIC ctxt' o known_ctac facts - ORELSE' refine_tac - ORELSE' sub_tac) i st) + ((NO_CONTEXT_TACTIC ctxt' o known_ctac facts THEN' K (debug_tac ctxt' "after `known`")) + ORELSE' (refine_tac THEN' K (debug_tac ctxt' "after `refine`")) + ORELSE' (sub_tac THEN' K (debug_tac ctxt' "after `sub`"))) i st) end and check_infer facts i (cst as (_, st)) = |