From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 02:36:08 +0000 (+0000)
Subject: Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
X-Git-Tag: make_still_working~3735
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=498898aa5d4525d979fe5564c180ab75f6483c99

Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
relaxed. Is this always correct??
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 87093e945..c19561d35 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -197,9 +197,9 @@ let does_not_occur ~subst context n nn t =
                perform substitution only if DoesOccur is raised *)
             let _,_,term,_ = U.lookup_subst mno subst in
             aux (k-s) () (S.subst_meta (0,l) term)
-          with U.Subst_not_found _ -> match l with
+          with U.Subst_not_found _ -> () (*match l with
           | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
-          | C.Ctx lc -> List.iter (aux (k-s) ()) lc)
+          | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
     | t -> U.fold (fun _ k -> k + 1) k aux () t
   in
    try aux 0 () t; true