bugfix that inhibit the removal of certain hypotheses

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 236ee28401fe6d2fba33d8d545dc890748baed4c..f08bb877a1029eac2d5ee939245e76d431a329e0 100644 (file)
--- 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) ->