Commit 5136e7e9 authored by Andrei Paskevich's avatar Andrei Paskevich

minor

parent e8691321
......@@ -173,7 +173,7 @@ exception ConstructorExpected of fsymbol
let pat_app fs pl ty =
if not fs.fs_constr then raise (ConstructorExpected fs);
let args, res = fs.fs_scheme in
ignore (try
ignore (try
List.fold_left2 Ty.matching
(Ty.matching Mid.empty res ty)
args (List.map (fun p -> p.pat_ty) pl)
......@@ -617,6 +617,7 @@ let f_v_any pr f = try f_v_fold (any_fn pr) 0 false f with FoldSkip -> true
let t_v_map fn = t_v_map fn 0
let f_v_map fn = f_v_map fn 0
let t_v_fold fn = t_v_fold fn 0
let f_v_fold fn = f_v_fold fn 0
......@@ -1077,6 +1078,7 @@ let f_open_branch (pat, _, f) =
(* safe opening map *)
let t_branch fn b = let pat,_,t = t_open_branch b in (pat, fn t)
let f_branch fn b = let pat,_,f = f_open_branch b in (pat, fn f)
let t_map fnT fnF t = t_label_try t.t_label (match t.t_node with
| Tbvar _ -> assert false
......@@ -1086,8 +1088,6 @@ let t_map fnT fnF t = t_label_try t.t_label (match t.t_node with
| Tcase (t1, bl) -> t_case (fnT t1) (List.map (t_branch fnT) bl) t.t_ty
| Teps b -> let u,f = f_open_bound b in t_eps u (fnF f))
let f_branch fn b = let pat,_,f = f_open_branch b in (pat, fn f)
let f_map fnT fnF f = f_label_try f.f_label (match f.f_node with
| Fapp (p, tl) -> f_app p (List.map fnT tl)
| Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
......
......@@ -140,8 +140,8 @@ exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition
exception UnboundVars of Svs.t
exception BadDecl of ident
let check_fvs f =
let fvs = f_freevars Svs.empty f in
......@@ -192,12 +192,10 @@ let create_type tdl =
let create_logic ldl =
let check_decl = function
| Lfunction (fs, Some fd) ->
let (s,_,_,_) = fd in
if fs != s then raise MalformedDefinition
| Lpredicate (ps, Some pd) ->
let (s,_,_,_) = pd in
if ps != s then raise MalformedDefinition
| Lfunction (fs, Some (s,_,_,_)) when s != fs ->
raise (BadDecl fs.fs_name)
| Lpredicate (ps, Some (s,_,_,_)) when s != ps ->
raise (BadDecl ps.ps_name)
| Linductive (ps,la) ->
let check_ax (_,f) =
ignore (check_fvs f);
......
......@@ -84,8 +84,8 @@ exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition
exception UnboundVars of Svs.t
exception BadDecl of ident
(** 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