Bug fixed: the debrujinate function (hence the one to compute objects height)

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 0f835961eeaef5353edd1eafa6110b8ee47e234f..d279b840b18d0fcc8602bff628677e7d32967dc3 100644 (file)
--- 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 =