From 00833b061a468bfda97a1514729d7048f89825ca Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jun 2018 16:36:37 +0200
Subject: [PATCH] Embarassing bug in eta_eq fixed

---
 ocaml/simple.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

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
-- 
2.39.2