From: Enrico Tassi <enrico.tassi@inria.fr>
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