Restrict reimplemented to avoid generating lists of indexes to be restricted

that fall outside the context. It doesn't change much, really.

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index aed59c5f4cf6fb01605e434d044a8955cb5db3aa..01b7d4a99247d6905665e9d850eb25fefb767d9f 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -42,7 +42,7 @@ let position n =
 
 exception Occur;;
 
-let rec force_does_not_occur k subst to_be_restricted t =
+let rec force_does_not_occur subst to_be_restricted t =
  let module C = Cic in
  let more_to_be_restricted = ref [] in
  let rec aux k = function
@@ -113,7 +113,7 @@ let rec force_does_not_occur k subst to_be_restricted t =
        in
        C.CoFix (i, fl')
  in
- let res = aux k t in
+ let res = aux 0 t in
  (!more_to_be_restricted, res)
  
 let rec restrict subst to_be_restricted metasenv =
@@ -121,28 +121,31 @@ let rec restrict subst to_be_restricted metasenv =
     String.concat ", "
       (List.map
         (fun i ->
-          match List.nth context i with
-          | None -> assert false
-          | Some (n, _) -> CicPp.ppname n)
-        indexes)
+          try
+           match List.nth context i with
+           | None -> assert false
+           | Some (n, _) -> CicPp.ppname n
+          with
+           Failure _ -> assert false
+        ) indexes)
   in
-  let force_does_not_occur_in_context k to_be_restricted = function
+  let force_does_not_occur_in_context to_be_restricted = function
     | None -> [], None
     | Some (name, Cic.Decl t) ->
         let (more_to_be_restricted, t') =
-          force_does_not_occur k subst to_be_restricted t
+          force_does_not_occur subst to_be_restricted t
         in
         more_to_be_restricted, Some (name, Cic.Decl t')
     | Some (name, Cic.Def (bo, ty)) ->
         let (more_to_be_restricted, bo') =
-          force_does_not_occur k subst to_be_restricted bo
+          force_does_not_occur subst to_be_restricted bo
         in
         let more_to_be_restricted, ty' =
           match ty with
           | None ->  more_to_be_restricted, None
           | Some ty ->
               let more_to_be_restricted', ty' =
-                force_does_not_occur k subst to_be_restricted ty
+                force_does_not_occur subst to_be_restricted ty
               in
               more_to_be_restricted @ more_to_be_restricted',
               Some ty'
@@ -161,7 +164,16 @@ let rec restrict subst to_be_restricted metasenv =
         else
           (try
             let more_to_be_restricted', hd' =
-              force_does_not_occur_in_context i restricted hd
+              let delifted_restricted =
+               let rec aux =
+                function
+                   [] -> []
+                 | j::tl when j > i -> (j - i)::aux tl
+                 | _::tl -> aux tl
+               in
+                aux restricted
+              in
+               force_does_not_occur_in_context delifted_restricted hd
             in
              more_to_be_restricted @ more_to_be_restricted',
              restricted, hd' :: tl'
@@ -183,14 +195,14 @@ let rec restrict subst to_be_restricted metasenv =
         in
         try
           let more_to_be_restricted', t' =
-            force_does_not_occur 0 subst restricted t
+            force_does_not_occur subst restricted t
           in
           let metasenv' = (n, context', t') :: metasenv in
           (try
             let s = List.assoc n subst in
             try
               let more_to_be_restricted'', s' =
-                force_does_not_occur 0 subst restricted s
+                force_does_not_occur subst restricted s
               in
               let subst' = (n, s') :: (List.remove_assoc n subst) in
               let more =