]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/num.ml
Fix: conv : x:min_int (.... y:1 ...) y was not considered for stepping
[fireball-separation.git] / ocaml / num.ml
index d00398532ae4495d6379a2fca1cc3e7f1adbf002..85a2bfa7583c6aaa82d70719ca5880da38207a32 100644 (file)
@@ -70,12 +70,12 @@ let rec make_lams t =
  | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)))
  | _ -> assert false
 
-let free_vars =
+let free_vars' =
  let rec aux n = function
     `N _ -> []
-  | `Var(x,_) -> if x < n then [] else [x-n]
-  | `I((x,_),args) ->
-      (if x < n then [] else [x-n]) @
+  | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
+  | `I((x,ar),args) ->
+      (if x < n then [] else [(x-n,ar)]) @
       List.concat (List.map (aux n) (Listx.to_list args))
   | `Lam(_,t) -> aux (n+1) t
   | `Match(t,_,liftno,bs,args) ->
@@ -84,6 +84,7 @@ let free_vars =
       List.concat (List.map (aux n) args)
   in aux 0
 ;;
+let free_vars = (List.map fst) ++ free_vars';;
 
 module ToScott =
 struct