]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/simple.ml
Simpler tests in simple_test.ml + Added diverging tests in simple.1
[fireball-separation.git] / ocaml / simple.ml
index b5a508691ea31dd83a8c930017df85d81f687b73..efa5c25d88fd47912ed7b5d656074a1c9bc685f9 100644 (file)
@@ -117,6 +117,7 @@ let rec no_leading_lambdas hd_var j = function
  | V n -> if n = hd_var then j else 0\r
  | B | C _ -> 0\r
 ;;\r
+\r
 let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r