From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2002 13:12:00 +0000 (+0000)
Subject: During the computation of the inner-type of a LAMBDA, the grandfather
X-Git-Tag: V_0_3_0_debian_8~172
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2bd948e245f117c1806390e9ddda149aa60df582;p=helm.git

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 789a72b91..677d633e5 100644
--- 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''