]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
paths trough terms implemented with a nice hack :)
[helm.git] / helm / ocaml / cic / cicUtil.ml
index 54bd178a0bed18232d5f153a5e82718d10cb73c3..5a64429a388da80c174e5ca3bfbce28a451f5ad5 100644 (file)
@@ -175,6 +175,7 @@ let select ~term ~context =
   let rec aux context term =
     match (context, term) with
     | Cic.Implicit (Some `Hole), t -> [t]
+    | Cic.Implicit None,_ -> []
     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
         List.concat
           (List.map2