added comment for zack

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c028b916f24d6e9d39ac53c93782ed840d0b2c31..42faf7e6ab6f2708672074802b9a79882b8ee36d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1013,8 +1013,7 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
  in
   match E.get_checked_obj uri, ref with
   | (_,_,_,_,C.Inductive(isind1,lno1,tl,_)),Ref.Ref(_,Ref.Ind (isind2,i,lno2))->
-      if isind1 <> isind2 then error ();
-      if lno1 <> lno2 then error ();
+      if isind1 <> isind2 || lno1 <> lno2 then error ();
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,lno1,tl,_)), Ref.Ref (_,Ref.Con (i,j,lno2))  ->
       if lno1 <> lno2 then error ();
@@ -1099,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
@@ -1108,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