summaryrefslogtreecommitdiff
path: root/src/initial_check.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-04-16 15:37:24 +0100
committerAlasdair Armstrong2018-04-18 14:17:26 +0100
commit7cab45aa4faac2990eb5e1991c0481b72e3c83ec (patch)
tree1cd5ad45157beb64837e5a7ac09351dce0602098 /src/initial_check.ml
parent127776db287e44521606debed8c4eaa125516c62 (diff)
Rename BK_nat to BK_int to be consistent with source syntax
Diffstat (limited to 'src/initial_check.ml')
-rw-r--r--src/initial_check.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b8c70e57..c6bc5fbe 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -149,7 +149,7 @@ let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l)
let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
match k with
| Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
- | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
+ | Parse_ast.BK_int -> BK_aux(BK_int,l'), { k = K_Nat }
| Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
@@ -1123,7 +1123,7 @@ let generate_enum_functions vs_ids (Defs defs) =
if IdSet.mem name vs_ids then []
else
[ enum_val_spec name
- [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)]
+ [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)]
(function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
mk_fundef [funcl] ]
in