From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 May 2008 23:42:25 +0000 (+0000)
Subject: Here is where we should add relevance checks.
X-Git-Tag: make_still_working~5138
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d1f0e3f90815a5afdf3b1412887628fb5107e267;p=helm.git

Here is where we should add relevance checks.
---

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