X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic%2FcicUtil.ml;h=405b183cf9ed41b042555621e837002d56002233;hb=244b44d6490eeb5f7cb89e83cfb6e22e9394ba11;hp=149a9bc2e1f2b028c7c30dfb0ed0d2d30984bc0b;hpb=e2fb8962f72096d3f0bb19f40b00a3502a11e932;p=helm.git

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 149a9bc2e..405b183cf 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -178,6 +178,7 @@ let select ~term ~context =
   let rec aux i context term =
     match (context, term) with
     | Cic.Implicit (Some `Hole), t -> [i,t]
+    | Cic.Implicit (Some `Type), t -> []
     | Cic.Implicit None,_ -> []
     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
         List.concat
@@ -209,7 +210,7 @@ let select ~term ~context =
           (List.map2
             (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2)
             funs1 funs2)
-    | _ -> assert false
+    | _ -> assert false (* maybe an Implicit annotation ? *)
   and auxs i terms1 terms2 =  (* as aux for list of terms *)
     List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2)
   in