Commit 680954f5 authored by Sylvain Dailler's avatar Sylvain Dailler

Remove compilation warnings

parent 517652cd
......@@ -9,11 +9,11 @@ let rec elim_quant pol f =
try
t_map_sign elim_quant pol f
with
Failure m -> f
Failure _m -> f
let elim_less (d:decl) =
match d.d_node with
| Dprop (Paxiom,v,t) ->
| Dprop (Paxiom,_v,t) ->
let t = elim_quant true t in
if t_equal t t_true then []
else
......
......@@ -9,8 +9,6 @@
(* *)
(********************************************************************)
open Ident
open Ty
open Term
open Decl
open Theory
......@@ -18,7 +16,7 @@ open Theory
let meta_elim_ls = register_meta "ls:eliminate" [MTlsymbol]
~desc:"Removes@ any@ expression@ containing@ a@ specific@ lsymbol."
let eliminate_symbol env =
let eliminate_symbol _env =
Trans.on_tagged_ls meta_elim_ls
(fun ls_elim ->
let elim_ls ls = Sls.exists (ls_equal ls) ls_elim in
......
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