From 04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Apr 2008 12:56:27 +0000 Subject: [PATCH] fixes backported from the new kernel --- .../components/cic_proof_checking/cicTypeChecker.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 7b98a59be..ad00c0eeb 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te = Failure _ -> assert false) | C.Sort _ | C.Implicit _ -> true - | C.Meta (_,l) -> + | C.Meta (mno,l) -> List.fold_right (fun x i -> match x with None -> i | 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 + let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term) with CicUtil.Subst_not_found _ -> true) @@ -1374,11 +1374,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let arity1 = CicReduction.whd ~subst context arity1 in let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy = match arity1, CicReduction.whd ~subst context arity2 with - (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> + (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger + ((Some (name,C.Decl so1))::context) uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 else @@ -2202,6 +2203,9 @@ let typecheck_obj0 ~logger uri ugraph = let _,ugraph = type_of ~logger ty ugraph in ugraph | C.CurrentProof (_,conjs,te,ty,_,_) -> + (* this block is broken since the metasenv should + * be topologically sorted before typing metas *) + ignore(assert false); let _,ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> -- 2.39.2