From: Stefano Zacchiroli Date: Mon, 1 Jul 2002 20:12:54 +0000 (+0000) Subject: bugfix that inhibit the removal of certain hypotheses X-Git-Tag: V_0_3_0_debian_8~12 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc883b40654c63af2a18d952986277e8e1d59cc9;p=helm.git bugfix that inhibit the removal of certain hypotheses --- diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 236ee2840..f08bb877a 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -134,12 +134,20 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts add_inner_type fresh_id'' ; C.AVar (fresh_id'', uri) | C.Meta (n,l) -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; C.AMeta (fresh_id'', n, - (List.map - (function None -> None | Some t -> Some (aux' context t)) l)) + (List.map2 + (fun ct t -> + match (ct, t) with + | None, _ -> None + | _, Some t -> Some (aux' context t) + | Some _, None -> assert false (* due to typing rules *)) + canonical_context l)) | C.Sort s -> C.ASort (fresh_id'', s) | C.Implicit -> C.AImplicit (fresh_id'') | C.Cast (v,t) ->