From: Stefano Zacchiroli <zack@upsilon.cc>
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) ->