Commit d00ac3d2 authored by MARCHE Claude's avatar MARCHE Claude

suppressed remaining compilation warnings

parent 714395e8
......@@ -71,7 +71,7 @@ EMACS = @EMACS@
#PDFVIEWER = @PDFVIEWER@
INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
WARNINGS = Aer-41-44-45@5
WARNINGS = Aer-41-44-45@5@48
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
......
......@@ -440,7 +440,7 @@ let e_ghostify gh ({e_effect = eff} as e) =
let c_ghostify gh ({c_cty = cty} as c) =
if cty.cty_effect.eff_ghost || not gh then c else
let el = match c.c_node with Cfun e -> [e] | _ -> [] in
mk_cexp c.c_node (try_effect el cty_ghostify gh cty)
mk_cexp c.c_node (try_effect el (cty_ghostify ?loc:None) gh cty)
(* let-definitions *)
......
......@@ -290,7 +290,9 @@ let create_module env ?(path=[]) n =
let add_pdecl ~wp uc d =
ignore wp; (* TODO *)
let uc = add_pdecl uc d in
let th = List.fold_left Theory.add_decl uc.muc_theory d.pd_pure in
let th =
List.fold_left (Theory.add_decl ~warn:false) uc.muc_theory d.pd_pure
in
{ uc with muc_theory = th }
let add_pdecl_with_tuples _uc _md = assert false (*TODO*)
......
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