]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicRefiner.ml
- hExtlib: added debugging information for split_nth
[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml
index ed14180aa670c7f41c6f8f28706ef53db6b4b419..68a1b2cbe983f0746a33e2fc9fe54b02de009ea7 100644 (file)
@@ -250,7 +250,7 @@ let rec typeof hdb
       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
       let metasenv, subst, term, _ = 
         typeof_aux metasenv subst context (Some ind) term in
-      let parameters, arguments = HExtlib.split_nth leftno args in
+      let parameters, arguments = HExtlib.split_nth "NR 1" leftno args in
       let outtype =  
         match outtype with
         | C.Implicit _ as ot -> 
@@ -614,20 +614,20 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj
       List.fold_left
        (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
          let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
-         let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
+         let sx_context_ty_rev,_= HExtlib.split_nth "NR 2" leftno (List.rev context) in
          let metasenv,subst,cl =
           List.fold_right
            (fun (k_relev,n,te) (metasenv,subst,res) ->
             let k_relev =
-              try snd (HExtlib.split_nth leftno k_relev)
+              try snd (HExtlib.split_nth "NR 3" leftno k_relev)
               with Failure _ -> k_relev in
              let te = NCicTypeChecker.debruijn uri len [] 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 =
-              HExtlib.split_nth (List.length tys) (List.rev context) in
+              HExtlib.split_nth "NR 4" (List.length tys) (List.rev context) in
              let sx_context_te_rev,_ =
-              HExtlib.split_nth leftno chopped_context_rev in
+              HExtlib.split_nth "NR 5" leftno chopped_context_rev in
              let metasenv,subst,_ =
               try
                List.fold_left2