X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=acb942ec5f37b9c4000a7b72c57e79a424b457eb;hb=0568c864d39f55fd2a32382bf5bc163edc0284b0;hp=637c346b06972b7dcc747ff4298414c2824e2899;hpb=aef0ab661736f065a2a41a09df6e79fd4e626cd7;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 637c346b0..acb942ec5 100644
--- 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