Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/typing.ml | ||
---|---|---|
647 | 647 |
let undefined_vars = |
648 | 648 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs |
649 | 649 |
in |
650 |
(* Typing asserts *) |
|
651 |
List.iter (fun assert_ -> |
|
652 |
let assert_expr = assert_.assert_expr in |
|
653 |
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool |
|
654 |
) nd.node_asserts; |
|
655 |
|
|
650 | 656 |
(* check that table is empty *) |
651 | 657 |
if (not (IMap.is_empty undefined_vars)) then |
652 | 658 |
raise (Error (loc, Undefined_var undefined_vars)); |
Also available in: Unified diff
Merged horn_traces branch