]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/num.ml
Moved parse' from Num to Parser
[fireball-separation.git] / ocaml / num.ml
index c88fa8de1a666cd68cbb8d1e5c10286fd38157f5..f612def74371072024552c584be261a8ff01ea69 100644 (file)
@@ -239,20 +239,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
   aux 0 where
 ;;
 
-(************ Parsing ************************************)
-
-let parse' strs =
-  let fix_arity = function
-  | `I((n,_),args) -> `I((n,1+Listx.length args),args)
-  | _ -> assert false in
-  let rec aux = function
-  | Parser.Lam t -> `Lam (true, aux t)
-  | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2))
-  | Parser.Var v -> `Var(v,1) in
-  let (tms, free) = Parser.parse_many strs in
-  List.map aux tms, free
-;;
-
 (************** Algorithm(s) ************************)
 
 let eta_compare x y =