Commit 4741f77d authored by MARCHE Claude's avatar MARCHE Claude

Fix wrong error message for bad arity

parent 2ff8efca
......@@ -219,9 +219,9 @@ let denv_add_pat denv dp =
(** Unification tools *)
let dty_unify_app ls unify l1 l2 =
let dty_unify_app ls unify (l1: 'a list) (l2:dty list) =
try List.iter2 unify l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l2))
raise (BadArity (ls, List.length l1))
let dpat_expected_type dp dty =
try dty_unify dp.dp_dty dty with Exit -> Loc.errorm ?loc:dp.dp_loc
......
......@@ -540,9 +540,9 @@ let denv_get_opt denv n =
(** Unification tools *)
let dity_unify_app ls fn l1 l2 =
let dity_unify_app ls fn l1 (l2:dity list) =
try List.iter2 fn l1 l2 with Invalid_argument _ ->
raise (BadArity (ls, List.length l2))
raise (BadArity (ls, List.length l1))
let dpat_expected_type {dp_dity = dp_dity; dp_loc = loc} dity =
try dity_unify dp_dity dity with Exit -> Loc.errorm ?loc
......
......@@ -7,6 +7,13 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
*)
theory W
use int.Int
predicate f (x:int) = Int.(<=) x
end
theory TestProp
......
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