From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jun 2018 14:36:37 +0000 (+0200)
Subject: Embarassing bug in eta_eq fixed
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00833b061a468bfda97a1514729d7048f89825ca;p=fireball-separation.git

Embarassing bug in eta_eq fixed
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index c7b9a3a..b1b05ec 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -21,19 +21,6 @@ type t =
  | L of t
 ;;
 
-let measure_of_t =
- let rec aux acc = function
- | V _ -> acc, 0
- | A(b,t1,t2) ->
-   let acc, m1 = aux acc t1 in
-   let acc, m2 = aux acc t2 in
-   (match b with
-   | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2
-   | _ -> acc, m1 + m2)
- | L t -> aux acc t
- in snd ++ (aux [])
-;;
-
 let index_of x =
  let rec aux n =
   function
@@ -88,6 +75,19 @@ let delta = L(A(`Some (ref true),V 0, V 0));;
 (* does NOT lift the argument *)
 let mk_lams = fold_nat (fun x _ -> L x) ;;
 
+let measure_of_t =
+ let rec aux acc = function
+ | V _ -> acc, 0
+ | A(b,t1,t2) ->
+   let acc, m1 = aux acc t1 in
+   let acc, m2 = aux acc t2 in
+   (match b with
+   | `Some b when !b && not (List.memq b acc) -> b::acc, 1 + m1 + m2
+   | _ -> acc, m1 + m2)
+ | L t -> aux acc t
+ in snd ++ (aux [])
+;;
+
 type problem = {
    orig_freshno: int
  ; freshno : int