From 498898aa5d4525d979fe5564c180ab75f6483c99 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:36:08 +0000 Subject: [PATCH] Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.) relaxed. Is this always correct?? --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2