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 1a899aaaaa1827e3ffe20a3a2522f13220dbf2b7..42faf7e6ab6f2708672074802b9a79882b8ee36d 100644 (file)
--- 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