fixed select (not Implicit (Some `TYPE) is handled)

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 149a9bc2e1f2b028c7c30dfb0ed0d2d30984bc0b..405b183cf9ed41b042555621e837002d56002233 100644 (file)
--- 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