From 0ddafb552e4653be302cac36554ebb5cfdac2be5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 15:58:46 +0000 Subject: [PATCH] add to the ids_to_father_ids table entries from hypothesis roots to hypothesis ids --- helm/ocaml/cic_acic/cic2acic.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/ocaml/cic_acic/cic2acic.ml b/helm/ocaml/cic_acic/cic2acic.ml index 194361622..79d9bd0da 100644 --- a/helm/ocaml/cic_acic/cic2acic.ml +++ b/helm/ocaml/cic_acic/cic2acic.ml @@ -400,10 +400,14 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids match binding with Some (n,Cic.Def (t,_)) -> let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in + Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) + (Some hid); (binding::context), ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs) | Some (n,Cic.Decl t) -> let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in + Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) + (Some hid); (binding::context), ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs) | None -> -- 2.39.2