snapshot for CSC

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c82fb457a2c4727bc8cf816729e53db9b4726e20..0904cf33119b99ff7183b998af6d1edbd95f01cb 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -538,9 +538,18 @@ let term_at i t =
 let src_tgt_of_ty_cpos_arity ty cpos arity =
   let pis = count_prod ty in
   let tpos = pis - arity in
-  let rec aux i j = function
+  let rec pi_nth i j = function
     | NCic.Prod (_,s,_) when i = j -> s
-    | NCic.Prod (_,_,t) -> aux (i+1) j t
+    | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
+    | t -> assert (i = j); t
+  in
+  let rec cleanup_prod = function
+    | NCic.Prod (_,_,t) -> NCic.Prod ("_",NCic.Implicit `Type, cleanup_prod t)
+    | _ -> NCic.Implicit `Type
+  in
+  let rec pi_tail i j = function
+    | NCic.Prod (_,_,_) as t when i = j -> cleanup_prod t
+    | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
     | t -> assert (i = j); t
   in
   let mask t =
@@ -552,7 +561,8 @@ let src_tgt_of_ty_cpos_arity ty cpos arity =
     in
      aux () t
   in 
-  mask (aux 0 cpos ty), mask (aux 0 tpos ty)
+  mask (pi_nth 0 cpos ty), 
+  mask (pi_tail 0 tpos ty)
 ;;
 
 let close_in_context t metasenv =