- NCicPp.ppterm applies the substitution

[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 cf445a8f0fc28d0d562238ecc053fd719186527c..806238ce3580330f7409289805b4bf655865334c 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -389,7 +389,7 @@ let rec typeof ~subst ~metasenv context term =
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
        let _ = typeof_aux context ty in
-       if not (R.are_convertible ~subst get_relevance context ty_t ty) then
+       if not (R.are_convertible ~subst context ty_t ty) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
@@ -460,7 +460,7 @@ let rec typeof ~subst ~metasenv context term =
               let ty_branch = 
                 type_of_branch ~subst context leftno outtype cons ty_cons 0 
               in
-              j+1, R.are_convertible ~subst get_relevance context ty_p ty_branch,
+              j+1, R.are_convertible ~subst context ty_p ty_branch,
               ty_p, ty_branch
             else
               j,false,old_p_ty,old_exp_p_ty
@@ -522,7 +522,7 @@ let rec typeof ~subst ~metasenv context term =
                 (_,C.Decl t1), (_,C.Decl t2)
               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
-                 if not (R.are_convertible ~subst get_relevance tl t1 t2) then
+                 if not (R.are_convertible ~subst tl t1 t2) then
                   raise 
                       (TypeCheckerFailure 
                         (lazy (Printf.sprintf 
@@ -573,7 +573,7 @@ let rec typeof ~subst ~metasenv context term =
                     with Failure _ -> t)
               | _ -> t
              in
-             if not (R.are_convertible ~subst get_relevance context optimized_t ct)
+             if not (R.are_convertible ~subst context optimized_t ct)
              then
                raise 
                  (TypeCheckerFailure 
@@ -584,7 +584,7 @@ let rec typeof ~subst ~metasenv context term =
                      (PP.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
-              if not (R.are_convertible ~subst get_relevance context type_t ct) then
+              if not (R.are_convertible ~subst context type_t ct) then
                 raise (TypeCheckerFailure 
                  (lazy (Printf.sprintf 
                   ("Not well typed metavariable local context: "^^
@@ -609,7 +609,7 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          if not (R.are_convertible ~subst get_relevance context so1 so2) then
+          if not (R.are_convertible ~subst context so1 so2) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context so1)
@@ -618,7 +618,7 @@ let rec typeof ~subst ~metasenv context term =
           aux ((name, C.Decl so1)::context)
            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-          if not (R.are_convertible ~subst get_relevance context so ind) then
+          if not (R.are_convertible ~subst context so ind) then
            raise (TypeCheckerFailure (lazy (Printf.sprintf
             "In outtype: expected %s, found %s"
             (PP.ppterm ~subst ~metasenv ~context ind)
@@ -659,7 +659,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   | (arg, ty_arg)::tl ->
       match R.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
-          if R.are_convertible ~subst get_relevance context ty_arg s then
+          if R.are_convertible ~subst context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
             raise 
@@ -736,11 +736,11 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
                 let convertible =
                  match item1,item2 with
                    (n1,C.Decl ty1),(n2,C.Decl ty2) ->
-                     n1 = n2 && R.are_convertible ~subst get_relevance context ty1 ty2
+                     n1 = n2 && R.are_convertible ~subst context ty1 ty2
                  | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
                      n1 = n2
-                     && R.are_convertible ~subst get_relevance context ty1 ty2
-                     && R.are_convertible ~subst get_relevance context bo1 bo2
+                     && R.are_convertible ~subst context ty1 ty2
+                     && R.are_convertible ~subst context bo1 bo2
                  | _,_ -> false
                 in
                  if not convertible then
@@ -1120,7 +1120,7 @@ let typecheck_context ~metasenv ~subst context =
        | name,C.Def (te,ty) ->
          ignore (typeof ~metasenv ~subst:[] context ty);
          let ty' = typeof ~metasenv ~subst:[] context te in
-          if not (R.are_convertible ~subst get_relevance context ty' ty) then
+          if not (R.are_convertible ~subst context ty' ty) then
            raise (AssertFailure (lazy (Printf.sprintf (
             "the type of the definiens for %s in the context is not "^^
             "convertible with the declared one.\n"^^
@@ -1158,7 +1158,7 @@ let typecheck_subst ~metasenv subst =
       typecheck_context ~metasenv ~subst context;
       ignore (typeof ~metasenv ~subst context ty);
       let ty' = typeof ~metasenv ~subst context bo in
-       if not (R.are_convertible ~subst get_relevance context ty' ty) then
+       if not (R.are_convertible ~subst context ty' ty) then
         raise (AssertFailure (lazy (Printf.sprintf (
          "the type of the definiens for %d in the substitution is not "^^
          "convertible with the declared one.\n"^^
@@ -1179,7 +1179,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
    | 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 get_relevance [] ty_te ty) then
+      if not (R.are_convertible ~subst [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf (
         "the type of the body is not convertible with the declared one.\n"^^
         "inferred type:\n%s\nexpected type:\n%s")
@@ -1211,7 +1211,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,_,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst get_relevance types ty_bo ty)
+       if not (R.are_convertible ~subst types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
        else
         if inductive then begin
@@ -1287,4 +1287,6 @@ E.set_typecheck_obj
     typecheck_obj obj)
 ;;
 
+let _ = NCicReduction.set_get_relevance get_relevance;;
+
 (* EOF *)