convertibility was taking a metasenv but not using it

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index a825e55d58e30653a7c5d5d0bae85438aaeb7066..bd2498c04e5b73d244e9e0ccc8ff45d294a9376d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -400,6 +400,8 @@ module Reduction(RS : Strategy) =
          if delta > height then config else 
            let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
            aux (0, [], body, s) 
+     | (_, _, NCic.Const (NReference.Ref (_,_,
+            (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
      | (_, _, NCic.Const (NReference.Ref 
            (height,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
         if delta > height then config else
@@ -418,7 +420,6 @@ module Reduction(RS : Strategy) =
                let _,_,_,_,body = List.nth fixes fixno in
                aux (0, [], body, new_s)
            | _ -> config)
-     | (_, _, NCic.Const _, _) as config -> config
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
@@ -487,7 +488,7 @@ let (===) x y = Pervasives.compare x y = 0 ;;
 module C = NCic
 
 (* t1, t2 must be well-typed *)
-let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
+let are_convertible whd ?(subst=[])  =
  let rec aux test_equality_only context t1 t2 =
    let rec aux2 test_equality_only t1 t2 =
      if t1 === t2 then

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 8c047c4c183d293a791d63f7e82c4b805623b08b..f83f3d45b8236c47af4d7a567cdc73659b4b7c3e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -29,7 +29,7 @@ val whd :
     NCic.term
 
 val are_convertible : 
-  ?subst:NCic.substitution -> ?metasenv:NCic.metasenv -> 
+  ?subst:NCic.substitution -> 
   NCic.context -> NCic.term -> NCic.term -> 
   bool
 

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