summaryrefslogtreecommitdiff
path: root/src/sail.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2017-07-12 13:09:46 +0100
committerThomas Bauereiss2017-07-12 13:09:46 +0100
commit4ba73e1e36a8ebda34d8d3afa6dbeff6256d262a (patch)
treed3f82b5062a02a73f70889aa0886986b1838f504 /src/sail.ml
parent3bdd45856d908432e3b0d1af3f480c2311818a7c (diff)
Add checks for variable identifiers in pattern subsumption
Diffstat (limited to 'src/sail.ml')
-rw-r--r--src/sail.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml
index d84144e1..e7a2bd99 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -174,7 +174,7 @@ let main() =
else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
else ());
(if !(opt_print_lem)
- then let ast_lem = rewrite_ast_lem ast in
+ then let ast_lem = rewrite_ast_lem type_envs ast in
if !(opt_libs_lem) = []
then output "" (Lem_out None) [out_name,ast_lem]
else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]