diff options
| author | Alasdair | 2019-03-05 23:54:07 +0000 |
|---|---|---|
| committer | Alasdair | 2019-03-05 23:54:07 +0000 |
| commit | 2cd88a225adf5f382df85a046cd59c43e1436965 (patch) | |
| tree | 3440fb50865043690157491884208e173c3a31b3 /src/specialize.ml | |
| parent | adf40a76fd9503628508ef1eea5396aabda88eab (diff) | |
Fix missing case in specialization
Diffstat (limited to 'src/specialize.ml')
| -rw-r--r-- | src/specialize.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/specialize.ml b/src/specialize.ml index a487fc2f..e2ab3c68 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -337,7 +337,8 @@ and remove_implicit_arg (A_aux (aux, l)) = let kopt_arg = function | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> arg_nexp (nvar kid) | KOpt_aux (KOpt_kind (K_aux (K_type,_), kid), _) -> arg_typ (mk_typ (Typ_var kid)) - | _ -> failwith "oh no" + | KOpt_aux (KOpt_kind (K_aux (K_bool, _), kid), _) -> arg_bool (nc_var kid) + | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) -> arg_order (mk_ord (Ord_var kid)) (* For numeric type arguments we have to be careful not to run into a situation where we have an instantiation like |
