From 5d0cc17962cb4fd16b1e198748f57b7a700b4156 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 Jun 2005 17:19:52 +0000 Subject: [PATCH] fixed select (not Implicit (Some `TYPE) is handled) --- helm/ocaml/cic/cicUtil.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2