From: Claudio Sacerdoti Coen Date: Fri, 15 May 2009 19:37:08 +0000 (+0000) Subject: Patch to add a debugging string to HExtlib.split_nth reverted X-Git-Tag: make_still_working~3976 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;p=helm.git Patch to add a debugging string to HExtlib.split_nth reverted (we cannot add a string to every function that raises an exception). To know where the problem is, it is sufficient to look at the backtrace. However: 1) it works for matitac -debug 2) ocaml is so dumb that it says "compile with -g" when it cannot find the executable in the current working directory. Since Matita chdir to the directory where the .ma file is, you need to put a copy of matitac (or make a symbolic link) where the .ma file is. --- diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 4ff411697..c8ff783c3 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -900,7 +900,7 @@ and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts in let x = List.nth tl cpos in let _,rest = - try HExtlib.split_nth "AC 1" (cpos + sats +1) tl with Failure _ -> [],[] + try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] in if rest = [] then acic2content diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index ee7ed08d0..fb8909152 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -151,7 +151,7 @@ let ast_of_acic0 ~output_type term_info acic k = | Some (_,_,_,sats,cpos) -> if cpos < List.length tl then let _,rest = - try HExtlib.split_nth "TAC 1" (cpos+sats+1) tl with Failure _ -> [],[] + try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] in if rest = [] then idref aid (List.nth (List.map k tl) cpos) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 7ac82a0a6..e41dd101b 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -64,8 +64,8 @@ let debug = ref false let split2_last l1 l2 = try let n = pred (List.length l1) in - let before1, after1 = HEL.split_nth "P2 1" n l1 in - let before2, after2 = HEL.split_nth "P2 2" n l2 in + let before1, after1 = HEL.split_nth n l1 in + let before2, after2 = HEL.split_nth n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" @@ -388,7 +388,7 @@ and proc_case st what uri tyno u v ts = let qs = proc_bkd_proofs (next st) synth names classes ts in let lpsno, _ = H.get_ind_type uri tyno in let ps, _ = H.get_ind_parameters st.context (H.cic v) in - let _, rps = HEL.split_nth "P2 3" lpsno ps in + let _, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in let e = Cn.mk_pattern rpsno u in let text = "" in diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 72cdab58c..a397de41e 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -148,7 +148,7 @@ and opt_appl g st es c t vs = let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in let csno, vsno = List.length classes, List.length vs in if csno < vsno then - let vvs, vs = HEL.split_nth "PO 1" csno vs in + let vvs, vs = HEL.split_nth csno vs in let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in opt_proof g (info st "Optimizer: anticipate 2") true c x else match conclusion, List.rev vs with @@ -185,7 +185,7 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases = let eliminator = H.get_default_eliminator c uri tyno outty in let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in let ps, sort_disp = H.get_ind_parameters c arg in - let lps, rps = HEL.split_nth "PO 2" lpsno ps in + let lps, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in if rpsno = 0 && sort_disp = 0 then (* FG: the transformation is not possible, we fall back into the plain case *) diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index f5bcee20b..65b5cea33 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.ml +++ b/helm/software/components/cic_proof_checking/cicDischarge.ml @@ -220,7 +220,7 @@ let rec discharge_term st t = match t with let vty = match vty with | C.Appl (C.MutInd (fu, fm, _) as hd :: args) when UM.eq fu u && fm = m && List.length args = psno -> - let largs, _ = X.split_nth "D 1" lpsno args in + let largs, _ = X.split_nth lpsno args in C.Appl (hd :: largs @ Ut.mk_rels rpsno 0) | _ -> assert false diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 07015ee8f..c38c15b93 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -367,7 +367,7 @@ and weakly_positive context n nn uri indparamsno posuri te = C.MutInd (uri',0,_) when UriManager.eq uri' uri -> dummy | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> - let _, rargs = HExtlib.split_nth "TC 1" leftno tl in + let _, rargs = HExtlib.split_nth leftno tl in if rargs = [] then dummy else Cic.Appl (dummy :: rargs) | C.Cast (te,ty) -> subst_inductive_type_with_dummy te | C.Prod (name,so,ta) -> @@ -753,7 +753,7 @@ and specialize_inductive_type ~logger ~subst ~metasenv context t = let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in (match o with | Cic.InductiveDefinition (tl,_,paramsno,_) -> - let left_args,_ = HExtlib.split_nth "TC 2" paramsno args in + let left_args,_ = HExtlib.split_nth paramsno args in List.map (fun (name, isind, arity, cl) -> let arity = CicSubstitution.subst_vars exp arity in let arity = instantiate_parameters left_args arity in @@ -1081,7 +1081,7 @@ and guarded_by_constructors ~logger ~subst ~metasenv indURI = ("Too many args for constructor: " ^ String.concat " " (List.map (fun x-> CicPp.ppterm x) args)))) in - let left, args = HExtlib.split_nth "TC 3" paramsno tl in + let left, args = HExtlib.split_nth paramsno tl in List.for_all (does_not_occur ~subst context n nn) left && analyse_instantiated_type rec_params args | C.Appl ((C.MutCase (_,_,out,te,pl))::_) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 537290dc6..b535b9ebe 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1553,7 +1553,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) let get_l_r_p n = function | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> - HExtlib.split_nth "R 1" n args + HExtlib.split_nth n args | _ -> assert false in let _, _, ty, cl = List.nth tl tyno in @@ -1626,7 +1626,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) (CR.head_beta_reduce ~delta:false (Cic.Appl [outty;k])))),k | Cic.Appl (Cic.MutInd _::pl) -> - let left_p,right_p = HExtlib.split_nth "R 2" leftno pl in + let left_p,right_p = HExtlib.split_nth leftno pl in let has_rights = right_p <> [] in let k = let k = Cic.MutConstruct (uri,tyno,i,[]) in @@ -1638,7 +1638,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) CicUniv.oblivion_ugraph with | Cic.Appl (Cic.MutInd _::args),_ -> - snd (HExtlib.split_nth "R 3" leftno args) + snd (HExtlib.split_nth leftno args) | _ -> assert false with CicTypeChecker.TypeCheckerFailure _-> assert false in @@ -1694,7 +1694,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) with | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ -> - snd (HExtlib.split_nth "R 4" leftno args), mty + snd (HExtlib.split_nth leftno args), mty | _ -> assert false with CicTypeChecker.TypeCheckerFailure _ -> raise (AssertFailure(lazy "already ill-typed matched term")) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 4d5ec86f5..fc3a47b5e 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -183,7 +183,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = in context2pres (match skip_initial_lambdas_internal with - Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context) + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) | _ -> p.Con.proof_context) presacontext in diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 4a228b232..b2092c5b3 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -267,11 +267,11 @@ let rec list_findopt f l = in aux 0 l -let split_nth msg n l = +let split_nth n l = let rec aux acc n l = match n, l with | 0, _ -> List.rev acc, l - | n, [] -> raise (Failure ("HExtlib.split_nth: " ^ msg)) + | n, [] -> raise (Failure "HExtlib.split_nth") | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in aux [] n l diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 52e2fbf60..20e6c0192 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -111,8 +111,7 @@ exception FailureAt of int * @returns two list, the first contains at least n elements, the second the * remaining ones * @raise Failure when List.length l < n *) -(* FG: first argument: error msg *) -val split_nth: string -> int -> 'a list -> 'a list * 'a list +val split_nth: int -> 'a list -> 'a list * 'a list (** skip [n] [l] skips the first n elements of l *) val list_skip : int -> 'a list -> 'a list diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml index 71fbcda7d..e949984e4 100644 --- a/helm/software/components/metadata/metadataDeps.ml +++ b/helm/software/components/metadata/metadataDeps.ml @@ -200,7 +200,7 @@ struct let neighbs = UriTbl.find adjlist uri in if Lazy.lazy_is_val neighbs.adjacency then begin let adjacency, _ = - HExtlib.split_nth "MD 1" neighbs.shown (Lazy.force neighbs.adjacency) + HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency) in List.iter (fun dest -> @@ -242,7 +242,7 @@ struct UriTbl.add adjlist dest neighborhood) adjacency; neighbs.shown <- weight; - fst (HExtlib.split_nth "MD 2" weight adjacency), weight + fst (HExtlib.split_nth weight adjacency), weight else begin (* nodes has been expanded at least once *) let adjacency = Lazy.force neighbs.adjacency in let total_nodes = List.length adjacency in @@ -251,7 +251,7 @@ struct let shown_before = neighbs.shown in neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes; let new_shown = neighbs.shown - shown_before in - (fst (HExtlib.split_nth "MD 3" new_shown (List.rev adjacency))), new_shown + (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown end else [], 0 (* all children are already shown *) end diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index aa7f84ad6..1815ceedf 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -164,7 +164,7 @@ module Reduction(RS : Strategy) = struct | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) -> aux (k, e, List.nth pl (j-1), s) | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')-> - let _,params = HExtlib.split_nth "NR 1" lno s' in + let _,params = HExtlib.split_nth lno s' in aux (k, e, List.nth pl (j-1), params@s) | _ -> config, true) in @@ -253,7 +253,7 @@ let are_convertible ~metasenv ~subst = let relevance = E.get_relevance r1 in let relevance = match r1 with | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth "NR 2" lno relevance in + let _,relevance = HExtlib.split_nth lno relevance in HExtlib.mk_list false lno @ relevance | _ -> relevance in @@ -265,13 +265,13 @@ let are_convertible ~metasenv ~subst = | HExtlib.FailureAt fail -> let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in - let _,relevance = HExtlib.split_nth "NR 3" fail relevance in + let _,relevance = HExtlib.split_nth fail relevance in let b,relevance = (match relevance with | [] -> assert false | b::tl -> b,tl) in if (not b) then - let _,tl1 = HExtlib.split_nth "NR 4" (fail+1) tl1 in - let _,tl2 = HExtlib.split_nth "NR 5" (fail+1) tl2 in + let _,tl1 = HExtlib.split_nth (fail+1) tl1 in + let _,tl2 = HExtlib.split_nth (fail+1) tl2 in try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux true context t1 t2) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 525261222..8beca4cf0 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -87,7 +87,7 @@ let fixed_args bos j n nn = | _::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *) | [],_::_ -> assert false in - let lefts, _ = HExtlib.split_nth "NTC 1" (min j (List.length args)) args in + let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in List.map (fun ((b,x),i) -> b && x = C.Rel (k-i)) (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts)) | t -> U.fold (fun _ k -> k+1) k aux acc t @@ -149,7 +149,7 @@ let specialize_inductive_type_constrs ~subst context ty_term = | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as ref) :: _ ) as ty -> let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in let _, leftno, itl, _, i = E.get_checked_indtys ref in - let left_args,_ = HExtlib.split_nth "NTC 2" leftno args in + let left_args,_ = HExtlib.split_nth leftno args in let _,_,_,cl = List.nth itl i in List.map (fun (rel,name,ty) -> rel, name, instantiate_parameters left_args ty) cl @@ -250,7 +250,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) when NUri.eq uri' uri -> - let _, rargs = HExtlib.split_nth "NTC 3" lno tl in + let _, rargs = HExtlib.split_nth lno tl in if rargs = [] then dummy else C.Appl (dummy :: rargs) | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t in @@ -291,7 +291,7 @@ and strictly_positive ~subst context n nn indparamsno posuri te = let _,paramsno,tyl,_,i = E.get_checked_indtys r in let _,name,ity,cl = List.nth tyl i in let ok = List.length tyl = 1 in - let params, arguments = HExtlib.split_nth "NTC 4" paramsno tl in + let params, arguments = HExtlib.split_nth paramsno tl in let lifted_params = List.map (S.lift 1) params in let cl = List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl @@ -341,7 +341,7 @@ let type_of_branch ~subst context leftno outty cons tycons = match R.whd ~subst context tycons with | C.Const (Ref.Ref (_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons] | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _))::tl) -> - let _,arguments = HExtlib.split_nth "NTC 5" leftno tl in + let _,arguments = HExtlib.split_nth leftno tl in C.Appl (S.lift liftno outty::arguments@[cons]) | C.Prod (name,so,de) -> let cons = @@ -453,7 +453,7 @@ let rec typeof ~subst ~metasenv context term = (PP.ppterm ~subst ~metasenv ~context ty) (PP.ppterm ~subst ~metasenv ~context (C.Const r'))))) else - try HExtlib.split_nth "NTC 6" leftno tl + try HExtlib.split_nth leftno tl with Failure _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf @@ -511,7 +511,7 @@ let rec typeof ~subst ~metasenv context term = = match l with | shift, C.Irl n -> - let context = snd (HExtlib.split_nth "NTC 7" shift context) in + let context = snd (HExtlib.split_nth shift context) in let rec compare = function | 0,_,[] -> () | 0,_,_::_ @@ -548,7 +548,7 @@ let rec typeof ~subst ~metasenv context term = compare (n,context,canonical_context) | shift, lc_kind -> (* we avoid useless lifting by shortening the context*) - let l,context = (0,lc_kind), snd (HExtlib.split_nth "NTC 8" shift context) in + let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in let lifted_canonical_context = let rec lift_metas i = function | [] -> [] @@ -689,7 +689,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty = let eaten = List.length args_with_ty - res in (C.Appl (he::List.map fst - (fst (HExtlib.split_nth "NTC 9" eaten args_with_ty))))))))) + (fst (HExtlib.split_nth eaten args_with_ty))))))))) in aux ty_he args_with_ty @@ -727,18 +727,18 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = (List.fold_right (fun (it_relev,_,ty,cl) i -> let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in - let sx_context_ty_rev,_ = HExtlib.split_nth "NTC 10" leftno (List.rev context) in + let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in List.iter (fun (k_relev,_,te) -> let k_relev = - try snd (HExtlib.split_nth "NTC 11" leftno k_relev) + try snd (HExtlib.split_nth leftno k_relev) with Failure _ -> k_relev in let te = debruijn uri len [] te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = - HExtlib.split_nth "NTC 12" (List.length tys) (List.rev context) in + HExtlib.split_nth (List.length tys) (List.rev context) in let sx_context_te_rev,_ = - HExtlib.split_nth "NTC 13" leftno chopped_context_rev in + HExtlib.split_nth leftno chopped_context_rev in (try ignore (List.fold_left2 (fun context item1 item2 -> @@ -896,7 +896,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let bo, context' = eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in let new_context_part,_ = - HExtlib.split_nth "NTC 14" (List.length context' - List.length context) + HExtlib.split_nth (List.length context' - List.length context) context' in let k = List.fold_right shift_k new_context_part new_k in let context, recfuns, x = k in @@ -968,7 +968,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = ("Too many args for constructor: " ^ String.concat " " (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args)))) in - let _, args = HExtlib.split_nth "NTC 15" paramsno tl in + let _, args = HExtlib.split_nth paramsno tl in analyse_instantiated_type rec_params args | C.Appl ((C.Match (_,out,te,pl))::_) | C.Match (_,out,te,pl) as t -> @@ -1119,7 +1119,7 @@ and get_relevance ~metasenv ~subst context t args = let eaten = List.length args - res in (C.Appl (t::fst - (HExtlib.split_nth "NTC 16" eaten args)))))))) + (HExtlib.split_nth eaten args)))))))) in aux context ty args ;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 6b78512bd..2738b1c90 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -258,7 +258,7 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ " " ^ CicPp.ppterm arity);*) match CicReduction.whd context tty with Cic.MutInd (_,_,ens) -> ens,[] | Cic.Appl (Cic.MutInd (_,_,ens)::args) -> - ens,fst (HExtlib.split_nth "ON 1" leftno args) + ens,fst (HExtlib.split_nth leftno args) | _ -> assert false in let rec aux n irl context outsort = diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 68a1b2cbe..ed14180aa 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -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 "NR 1" leftno args in + let parameters, arguments = HExtlib.split_nth 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 "NR 2" leftno (List.rev context) in + let sx_context_ty_rev,_= HExtlib.split_nth 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 "NR 3" leftno k_relev) + try snd (HExtlib.split_nth 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 "NR 4" (List.length tys) (List.rev context) in + HExtlib.split_nth (List.length tys) (List.rev context) in let sx_context_te_rev,_ = - HExtlib.split_nth "NR 5" leftno chopped_context_rev in + HExtlib.split_nth leftno chopped_context_rev in let metasenv,subst,_ = try List.fold_left2 diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 09d9ede47..59bc5d7e7 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -65,7 +65,7 @@ let eta_reduce subst t = | Some bo -> aux (ctx,bo)) | (name, src)::ctx, (NCic.Appl args as bo) when HExtlib.list_last args = NCic.Rel 1 -> - let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in + let args, _ = HExtlib.split_nth (List.length args - 1) args in (match delift_if_not_occur (NCic.Appl args) with | None -> aux (ctx,NCic.Lambda(name,src, bo)) | Some bo -> aux (ctx,bo)) @@ -418,7 +418,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let relevance = match r1 with | Ref.Ref (_,Ref.Con (_,_,lno)) -> let relevance = - try snd (HExtlib.split_nth "NU 2" lno relevance) + try snd (HExtlib.split_nth lno relevance) with Failure _ -> [] in HExtlib.mk_list false lno @ relevance diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 29eee6b7b..323b1e6fc 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -320,7 +320,7 @@ let analyse_indty status ty = let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in let _,_,_,cl = List.nth tl i in let consno = List.length cl in - let left, right = HExtlib.split_nth "NTS 1" lno args in + let left, right = HExtlib.split_nth lno args in status, (ref, consno, left, right) ;; diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 07308b407..2c67c95ee 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -199,7 +199,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= let l_c2 = skip_appl (purge_lambdas term) in let l_c2_b,l_c2_a = try - HExtlib.split_nth "CCG 1" (c2_pis - sat2 - 1) l_c2 + HExtlib.split_nth (c2_pis - sat2 - 1) l_c2 with Failure _ -> assert false in let l_c1,l_c2_a = diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index c658e2cc9..f6fb61ac1 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/components/tactics/destructTactic.ml @@ -305,7 +305,7 @@ let injection_tac ~lterm ~i ~continuation ~recur = let patterns,outtype = match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with | C.InductiveDefinition (ind_type_list,_,paramsno,_)-> - let left_params, right_params = HExtlib.split_nth "DT 1" paramsno params in + let left_params, right_params = HExtlib.split_nth paramsno params in let _,_,_,constructor_list = List.nth ind_type_list typeno in let i_constr_id,_ = List.nth constructor_list (consno - 1) in let patterns = @@ -354,7 +354,7 @@ let injection_tac ~lterm ~i ~continuation ~recur = match S.lift 1 tty with | C.MutInd _ as tty' -> tty' | C.Appl l -> - let keep,abstract = HExtlib.split_nth "DT 2" (paramsno +1) l in + let keep,abstract = HExtlib.split_nth (paramsno +1) l in let keep = List.map (S.lift paramsno) keep in C.Appl (keep@mk_rels (List.length abstract)) | _ -> assert false