Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
b57a096e
Commit
b57a096e
authored
Feb 13, 2013
by
MARCHE Claude
Browse files
removed a few ocaml 4.00 warnings
parent
d82953a2
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/parser/lexer.mll
View file @
b57a096e
...
...
@@ -12,8 +12,7 @@
{
open
Format
open
Lexing
open
Term
open
Parser
open
Parser
(* lexical errors *)
...
...
src/parser/typing.ml
View file @
b57a096e
...
...
@@ -34,7 +34,9 @@ exception ClashTheory of string
exception UnboundTheory of qualid
*)
exception
UnboundTypeVar
of
string
(* dead code
exception UnboundType of string list
*)
exception
UnboundSymbol
of
string
list
let
error
=
Loc
.
error
...
...
@@ -66,8 +68,10 @@ let () = Exn_printer.register (fun fmt e -> match e with
*)
|
UnboundTypeVar
s
->
fprintf
fmt
"unbound type variable '%s"
s
(* dead code
| UnboundType sl ->
fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
*)
|
UnboundSymbol
sl
->
fprintf
fmt
"Unbound symbol '%a'"
(
print_list
dot
pp_print_string
)
sl
|
_
->
raise
e
)
...
...
@@ -121,12 +125,16 @@ type denv = {
let
denv_empty
=
{
dvars
=
Mstr
.
empty
;
gvars
=
Util
.
const
None
}
let
denv_empty_with_globals
gv
=
{
dvars
=
Mstr
.
empty
;
gvars
=
gv
}
(* dead code
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
*)
let
add_var
x
ty
denv
=
{
denv
with
dvars
=
Mstr
.
add
x
ty
denv
.
dvars
}
(* dead code
let print_denv fmt denv =
Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars
*)
(* parsed types -> intermediate types *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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