Bug fixed: restriction of already restricted contexts was bugged (due to

a missing "incr i").

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 637c346b06972b7dcc747ff4298414c2824e2899..acb942ec5f37b9c4000a7b72c57e79a424b457eb 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -56,13 +56,15 @@ let rec force_does_not_occur subst to_be_restricted t =
        let l' =
          let i = ref 0 in
          List.map
-           (function
-             | None -> None
-             | Some t ->
-                 incr i;
+           (function t ->
+             incr i ;
+             match t with
+                None -> None
+              | Some t ->
                  try
                    Some (aux k t)
                  with Occur ->
+prerr_endline (Printf.sprintf "RESTRINGO (%d,%d)" n !i) ;
                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
                    None)
            l