During the computation of the inner-type of a LAMBDA, the grandfather

was retrieved instead of the father. Fixed.

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 789a72b91a34cb9b9b85e240272acc93c538589a..677d633e51215050687132a951ee6f5f277b22d3 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -119,12 +119,9 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
               match father with
                  None -> false
                | Some father' ->
-                  match Hashtbl.find ids_to_father_ids father' with
-                     None -> assert false
-                   | Some fatherid ->
-                      match Hashtbl.find ids_to_terms fatherid with
-                         C.Lambda _ -> true
-                       | _ -> false
+                  match Hashtbl.find ids_to_terms father' with
+                     C.Lambda _ -> true
+                   | _ -> false
              in
               if not father_is_lambda then
                add_inner_type fresh_id''