diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 |
6 files changed, 11 insertions, 11 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f3e414126b..0dbaccc336 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -396,7 +396,7 @@ let clenv_independent clenv = List.filter (fun mv -> not (Metaset.mem mv deps)) mvs let check_bindings bl = - match list_duplicates (List.map pi2 bl) with + match List.duplicates (List.map pi2 bl) with | NamedHyp s :: _ -> errorlabstrm "" (str "The variable " ++ pr_id s ++ @@ -464,7 +464,7 @@ exception NoSuchBinding let clenv_constrain_last_binding c clenv = let all_mvs = collect_metas clenv.templval.rebus in - let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in + let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k c let error_not_right_number_missing_arguments n = diff --git a/proofs/logic.ml b/proofs/logic.ml index dcf1e4c733..53f5705a5a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -308,7 +308,7 @@ let collect_meta_variables c = List.rev (collrec false [] c) let check_meta_variables c = - if not (list_distinct (collect_meta_variables c)) then + if not (List.distinct (collect_meta_variables c)) then raise (RefinerError (NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = @@ -536,7 +536,7 @@ let prim_refiner r sigma goal = | _ -> error "Not enough products." in let (sp,_) = check_ind env n cl in - let firsts,lasts = list_chop j rest in + let firsts,lasts = List.chop j rest in let all = firsts@(f,n,cl)::lasts in let rec mk_sign sign = function | (f,n,ar)::oth -> @@ -580,7 +580,7 @@ let prim_refiner r sigma goal = error ("All methods must construct elements " ^ "in coinductive types.") in - let firsts,lasts = list_chop j others in + let firsts,lasts = List.chop j others in let all = firsts@(f,cl)::lasts in List.iter (fun (_,c) -> check_is_coind env c) all; let rec mk_sign sign = function diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index f7d9446b51..ab80841d8b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -126,7 +126,7 @@ let solve_nth ?(with_end_tac=false) gi tac = Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) with | Proof_global.NoCurrentProof -> Errors.error "No focused proof" - | Proofview.IndexOutOfRange | Failure "list_chop" -> + | Proofview.IndexOutOfRange | Failure "List.chop" -> let msg = str "No such goal: " ++ int gi ++ str "." in Errors.errorlabstrm "" msg diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 0e2ac1ddef..79b5ae7310 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -112,7 +112,7 @@ let focus_sublist i j l = let (left,sub_right) = list_goto (i-1) l in let (sub, right) = try - Util.list_chop (j-i+1) sub_right + Util.List.chop (j-i+1) sub_right with Failure "list_chop" -> Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal") in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 75a2ae8c38..c16e02b3fb 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -56,9 +56,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - list_smartmap + List.smartmap (fun (k,ql as entry) -> - let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 910653ddb8..0652f19864 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -109,7 +109,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let ng = List.length gs in if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals."); let gll = - (list_map_i (fun i -> + (List.map_i (fun i -> apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) 0 gs) in (sigr,List.flatten gll) @@ -123,7 +123,7 @@ let thensl_tac tac taci = thens3parts_tac [||] tac taci (* Apply [tac i] on the ith subgoal (no subgoals number check) *) let thensi_tac tac (sigr,gs) = let gll = - list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in (sigr, List.flatten gll) let then_tac tac = thensf_tac [||] tac |