From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 22:22:44 +0000 (+0000)
Subject: Bug fixed: restriction of already restricted contexts was bugged (due to
X-Git-Tag: V_0_2_3~62
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0568c864d39f55fd2a32382bf5bc163edc0284b0;p=helm.git

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