convertibility was taking a metasenv but not using it

[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 7e0f483d301adf6773d5bc4e9822a291caa40113..efe04de1a7553d3b43d44b7a1c0c069447a33485 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -151,7 +151,7 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
           prerr_endline (PP.ppterm ~subst ~metasenv ~context
              (S.subst ~avoid_beta_redexes:true arg t));
 *)
-          if R.are_convertible ~subst ~metasenv 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 
@@ -393,7 +393,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 ~metasenv context ty ty_t) then
+       if not (R.are_convertible ~subst context ty ty_t) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
@@ -471,7 +471,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 ~metasenv 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
@@ -533,7 +533,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 ~metasenv tl t1 t2) then
+                 if not (R.are_convertible ~subst tl t1 t2) then
                   raise 
                       (TypeCheckerFailure 
                         (lazy (Printf.sprintf 
@@ -584,7 +584,7 @@ let rec typeof ~subst ~metasenv context term =
                     with Failure _ -> t)
               | _ -> t
              in
-             if not (R.are_convertible ~subst ~metasenv context optimized_t ct)
+             if not (R.are_convertible ~subst context optimized_t ct)
              then
                raise 
                  (TypeCheckerFailure 
@@ -595,7 +595,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 ~metasenv 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: "^^
@@ -630,7 +630,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 ~metasenv 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)
@@ -639,7 +639,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 ~metasenv 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)
@@ -979,7 +979,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
    | C.Constant (_,_,Some te,ty,_) ->
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-      if not (R.are_convertible ~subst ~metasenv [] 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")
@@ -1006,7 +1006,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,name,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst ~metasenv 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