X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=8872cbc9b576f855a8f65334addc871864e3bc6c;hb=0e135d52a8c1b825a7844b897546bb7ae4af44d2;hp=0f835961eeaef5353edd1eafa6110b8ee47e234f;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 0f835961e..8872cbc9b 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -376,8 +376,7 @@ and try_coercions rdb
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
     first exc
-      (NCicCoercion.look_for_coercion 
-        rdb.NRstatus.coerc_db metasenv subst context infty expty)
+      (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
   match NCicReduction.whd ~subst context ty with
@@ -559,7 +558,6 @@ let undebruijnate inductive ref t rev_fl =
 let typeof_obj 
   rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
 = 
-prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
   let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
     let metasenv, subst, ty, sort = 
       typeof rdb ~localise metasenv subst context ty None
@@ -576,8 +574,7 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj
          match bo with
          | Some bo ->
              let metasenv, subst, bo, ty = 
-               typeof rdb ~localise metasenv subst [] bo (Some ty)
-             in
+               typeof rdb ~localise metasenv subst [] bo (Some ty) in
              let height = (* XXX recalculate *) height in
                metasenv, subst, Some bo, ty, height
          | None -> metasenv, subst, None, ty, 0
@@ -590,7 +587,7 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj
         List.fold_left
          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
            let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
-           let dbo = NCicTypeChecker.debruijn uri len [] bo in
+           let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in
            let localise = relocalise localise dbo bo in
             (name,C.Decl ty)::types,
               metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
@@ -639,7 +636,7 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj
 	     let k_relev =
               try snd (HExtlib.split_nth leftno k_relev)
               with Failure _ -> k_relev in
-             let te = NCicTypeChecker.debruijn uri len [] te in
+             let te = NCicTypeChecker.debruijn uri len [] ~subst te in
              let metasenv, subst, te, _ = check_type metasenv subst tys te in
              let context,te = NCicReduction.split_prods ~subst tys leftno te in
              let _,chopped_context_rev =
@@ -717,7 +714,8 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj
                 raise
                   (RefineFailure
                     (lazy (localise te,
-                      "Non positive occurence in " ^ NUri.string_of_uri uri)))
+                      "Non positive occurence in " ^
+                        NCicPp.ppterm ~metasenv ~subst ~context te)))
               else
                let relsno = List.length itl + leftno in
                let te =