From: Claudio Sacerdoti Coen 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