Commit 4cebacb3 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

cannot define a constructor fsymbol

parent 7e7f732d
......@@ -133,9 +133,11 @@ let create_prop k i f = Hdecl.hashcons (mk_decl (Dprop (k, id_register i, f)))
(* error reporting *)
exception NotAConstructor of fsymbol
exception MalformedDefinition of fmla
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition of fmla
exception UnboundVars of Svs.t
let make_fdef fs vl t =
......@@ -189,6 +191,7 @@ let create_logic ldl =
in
let check_decl = function
| Lfunction (fs, Some fd) ->
if fs.fs_constr then raise (IllegalConstructor fs);
let (vl,_,f) = check_def fd in
let hd = match f.f_node with
| Fapp (ps, [hd; _]) when ps == ps_equ -> hd
......
......@@ -71,9 +71,11 @@ val create_prop : prop_kind -> preid -> fmla -> decl
(* exceptions *)
exception NotAConstructor of fsymbol
exception MalformedDefinition of fmla
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition of fmla
exception UnboundVars of Svs.t
(** Theory *)
......
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