diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index d58f38d4..f6717ea4 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1835,12 +1835,10 @@ let is_nat_kid kid = function let is_order_kid kid = function | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0 - | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 | _ -> false let is_typ_kid kid = function | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0 - | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 | _ -> false let rec instantiate_quants quants kid uvar = match quants with |