X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=3df3dc3549ea5cda47b0a891627fb52a694f5f0e;hb=3add6ac24088e2a1d91a41123f433e2c2b0b796a;hp=c4b7f8cbf6f8a521c8f1d7fc3682b0a3aecfd39b;hpb=fecaa410b6226e8614cfef78d0f952e3c676c06e;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c4b7f8cbf..3df3dc354 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -240,12 +240,16 @@ and type_of_variable ~logger uri ugraph =
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
-   (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
-   (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
-   (*CSC: universi                                                    *)
-   match CicReduction.whd ~subst context te with
+   match te with
       C.Rel m when m > n && m <= nn -> false
-    | C.Rel _
+    | C.Rel m ->
+       (try
+         (match List.nth context (m-1) with
+             Some (_,C.Def (bo,_)) ->
+              does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
+           | _ -> true)
+        with
+         Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
     | C.Meta (_,l) ->
@@ -253,7 +257,12 @@ and does_not_occur ?(subst=[]) context n nn te =
         (fun x i ->
           match x with
              None -> i
-           | Some x -> i && does_not_occur ~subst context n nn x) l true
+           | Some x -> i && does_not_occur ~subst context n nn x) l true &&
+       (try
+         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+          does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
+        with
+         CicUtil.Subst_not_found _ -> true)
     | C.Cast (te,ty) ->
        does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->