From 2bd948e245f117c1806390e9ddda149aa60df582 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 8 Apr 2002 13:12:00 +0000 Subject: [PATCH] During the computation of the inner-type of a LAMBDA, the grandfather was retrieved instead of the father. Fixed. --- helm/gTopLevel/cic2acic.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) 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'' -- 2.39.2