Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
0ef80f1a
Commit
0ef80f1a
authored
Sep 14, 2011
by
Jean-Christophe Filliâtre
Browse files
old not allowed in programs
parent
0f220a20
Changes
2
Hide whitespace changes
Inline
Side-by-side
bench/programs/bad-typing/old3.mlw
0 → 100644
View file @
0ef80f1a
(* old not allowed in programs *)
module Test
use import module ref.Refint
let test (x: ref int) =
if !x = old !x then 1 else 2
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/old3"
End:
*)
\ No newline at end of file
src/programs/pgm_typing.ml
View file @
0ef80f1a
...
...
@@ -410,6 +410,7 @@ and dexpr_desc ~ghost env loc = function
with
Not_found
->
errorm
~
loc
"unbound symbol %a"
print_qualid
p
in
if
ls_equal
ls
fs_old
then
errorm
~
loc
"old not allowed in programs"
;
let
ps
=
get_psymbol
ls
in
begin
match
ps
.
ps_kind
with
|
PSvar
v
->
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment