From fb153b0a3853478410bfbcad98065f1b1610d17d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Feb 2004 16:40:29 +0000 Subject: [PATCH] sort_of_prod now thinks that a "sort metavariable" is a metavariable where no free variable occurs in the local context. Reason: there used to be a bug induced by the fact that a metavariable ?1 with an empty canonical context could be istantiated with a metavariable ?2[l] where l has no free variables but still it is not of length 0. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 8403f5f0c..9c9c0e58c 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -203,7 +203,7 @@ and does_not_occur context n nn te = match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> false | C.Rel _ - | C.Meta _ + | C.Meta _ (* CSC: Are we sure? No recursion?*) | C.Sort _ | C.Implicit _ -> true | C.Cast (te,ty) -> @@ -1294,7 +1294,8 @@ and check_metasenv_consistency metasenv context canonical_context l = | (Some (n,C.Def (t,None)))::tl -> (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (_,Some _)))::_ -> assert false + | (Some (n,C.Def (t,Some ty)))::tl -> + (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1638,8 +1639,9 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) | (C.Meta _, C.Sort _) -> t2' - | (C.Meta _, C.Meta (_,[])) - | (C.Sort _, C.Meta (_,[])) -> t2' + | (C.Meta _, (C.Meta (_,_) as t)) + | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> + t2' | (_,_) -> raise (TypeCheckerFailure (sprintf "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) -- 2.39.2