diff options
| author | Brian Campbell | 2018-04-20 14:13:30 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-04-20 14:13:30 +0100 |
| commit | 895f868cd537277ba61dfc427fee0e288af7e226 (patch) | |
| tree | f7f406b4ec55daf0f8f9339576dba6a404a260c6 /src | |
| parent | 83b7f7065c638ed3b0e0c40a5c4b64257bae4975 (diff) | |
Allow instantiation of type or order type variables without kind declaration
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 9de6d7e7..cad7dc47 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1861,10 +1861,12 @@ 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 |