Commit 7ac0a5a7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

= replaced by ls_equal in core/pretty (was discovered thanks to a...

= replaced by ls_equal in core/pretty (was discovered thanks to a Invalid_argument(equal: functional value)
parent 1bc159fb
...@@ -216,7 +216,7 @@ and print_tnode pri fmt t = match t.t_node with ...@@ -216,7 +216,7 @@ and print_tnode pri fmt t = match t.t_node with
forget_var v forget_var v
and print_fnode pri fmt f = match f.f_node with and print_fnode pri fmt f = match f.f_node with
| Fapp (ps,[t1;t2]) when ps = ps_equ -> | Fapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
fprintf fmt (protect_on (pri > 4) "%a =@ %a") fprintf fmt (protect_on (pri > 4) "%a =@ %a")
(print_lterm 4) t1 (print_lterm 4) t2 (print_lterm 4) t1 (print_lterm 4) t2
| Fapp (ps,[]) -> | Fapp (ps,[]) ->
......
...@@ -83,7 +83,7 @@ let dty_bool gl = dty_app (gl.ts_bool, []) ...@@ -83,7 +83,7 @@ let dty_bool gl = dty_app (gl.ts_bool, [])
let dty_unit gl = dty_app (gl.ts_unit, []) let dty_unit gl = dty_app (gl.ts_unit, [])
let dty_label gl = dty_app (gl.ts_label, []) let dty_label gl = dty_app (gl.ts_label, [])
(* note: local variables are sqimultaneously in locals (to type programs) (* note: local variables are simultaneously in locals (to type programs)
and in denv (to type logic elements) *) and in denv (to type logic elements) *)
type denv = { type denv = {
env : env; env : env;
......
...@@ -11,6 +11,11 @@ let f () = ...@@ -11,6 +11,11 @@ let f () =
r := 1; r := 1;
assert { !r > 0 } assert { !r > 0 }
let foo () =
let x = any {} int {result=0} in
let y = any {} int {result=result+1} in
assert { false }
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C .. testl" compile-command: "unset LANG; make -C .. testl"
......
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