Commit f9dcce6b authored by Andrei Paskevich's avatar Andrei Paskevich

minor

parent d7477cf4
......@@ -435,8 +435,8 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
ignore (option_map (ity_v_all Util.ttrue check) def);
(* if a type is an alias then it cannot be abstract or private *)
if abst && def <> None then Loc.errorm "Type alias cannot be abstract";
if priv && def <> None then Loc.errorm "Type alias cannot be private";
if abst && def <> None then Loc.errorm "A type alias cannot be abstract";
if priv && def <> None then Loc.errorm "A type alias cannot be private";
{ its_pure = purets;
its_args = args;
its_regs = regs;
......
......@@ -1400,9 +1400,9 @@ let add_module lib path mm mt m =
let uc = create_module ~path (Denv.create_user_id m.mod_name) in
let rec add_decl uc (loc,decl) = match decl with
| Dlogic (TypeDecl tdl) ->
add_types uc tdl
Loc.try2 loc add_types uc tdl
| Dlogic d ->
add_to_theory Typing.add_decl uc d
Loc.try3 loc add_to_theory Typing.add_decl uc d
| Duseclone (use, inst) ->
let path, s = Typing.split_qualid use.use_theory in
let mth = find_module loc lib mm mt path s in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment