From: Enrico Tassi Date: Fri, 24 Jun 2005 17:19:52 +0000 (+0000) Subject: fixed select (not Implicit (Some `TYPE) is handled) X-Git-Tag: INDEXING_NO_PROOFS~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d0cc17962cb4fd16b1e198748f57b7a700b4156;p=helm.git fixed select (not Implicit (Some `TYPE) is handled) --- 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