From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2017 13:36:56 +0000 (+0200)
Subject: Hack to reserve var 0 to purify it to BOM removed
X-Git-Tag: weak-reduction-separation~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=317fcb4eb9b89d617ab76cbded0c4654b67cfe16;p=fireball-separation.git

Hack to reserve var 0 to purify it to BOM removed

(cherry picked from commit 1fdb461d0bc4056ade8a05c482142984dbda735c)
---

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 1e69acb..8ba2fbd 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -118,13 +118,11 @@ let parse x =
   | _, _, _ -> raise (ParsingError "???")
 ;;
 
-let var_zero = "Z";; (* the name for the zero *)
-
 let parse_many strs =
   let f (x, y) z = match read_smt y (explode z) with
   | Some[tm], [], vars -> (tm :: x, vars)
   | _, _, _ -> raise (ParsingError "???")
-  in let aux = List.fold_left f ([], ([], [var_zero])) (* index zero is reserved *)
+  in let aux = List.fold_left f ([], ([], [])) (* index zero is reserved *)
   in let (tms, (_, free)) = aux strs
   in (List.rev tms, free)
 ;;