From d1f0e3f90815a5afdf3b1412887628fb5107e267 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 May 2008 23:42:25 +0000 Subject: [PATCH] Here is where we should add relevance checks. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 1a899aaaa..42faf7e6a 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -1098,7 +1098,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = typecheck_metasenv metasenv; typecheck_subst ~metasenv subst; match kind with - | C.Constant (_,_,Some te,ty,_) -> + | C.Constant (relevance,_,Some te,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in let ty_te = typeof ~subst ~metasenv [] te in if not (R.are_convertible ~subst [] ty_te ty) then @@ -1107,13 +1107,14 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = "inferred type:\n%s\nexpected type:\n%s") (PP.ppterm ~subst ~metasenv ~context:[] ty_te) (PP.ppterm ~subst ~metasenv ~context:[] ty)))) - | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) + | C.Constant (relevance,_,None,ty,_) -> + ignore (typeof ~subst ~metasenv [] ty) | C.Inductive (is_ind, leftno, tyl, _) -> check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl | C.Fixpoint (inductive,fl,_) -> let types, kl = List.fold_left - (fun (types,kl) (_,name,k,ty,_) -> + (fun (types,kl) (relevance,name,k,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in ((name,C.Decl ty)::types, k::kl) ) ([],[]) fl -- 2.39.2