From 0568c864d39f55fd2a32382bf5bc163edc0284b0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 22:22:44 +0000
Subject: [PATCH] Bug fixed: restriction of already restricted contexts was
 bugged (due to a missing "incr i").

---
 helm/ocaml/cic_unification/cicMetaSubst.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

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
-- 
2.39.2