diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-23 15:05:26 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-23 15:05:26 +0000 |
| commit | 914d19f19cd73d1794c0160bd6e7358c13eba630 (patch) | |
| tree | c60b68ddac62f60f1bef763ba970805d228180ad /tactics | |
| parent | 7bc3e1ce35798d089a979f3cb5a4c5ecc232f850 (diff) | |
Minor code cleaning in CArray / CList.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
3 files changed, 6 insertions, 7 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index f9b45bdfb..e05c5384a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -873,10 +873,9 @@ let interp_hints = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; - List.tabulate (fun i -> let c = (ind,i+1) in + List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - None, true, PathHints [gr], IsGlobal gr) - (nconstructors ind) in + None, true, PathHints [gr], IsGlobal gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in @@ -1069,7 +1068,7 @@ let expand_constructor_hints env lems = List.map_append (fun (sigma,lem) -> match kind_of_term lem with | Ind ind -> - List.tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind) + List.init (nconstructors ind) (fun i -> mkConstruct (ind,i+1)) | _ -> [prepare_hint env (sigma,lem)]) lems diff --git a/tactics/inv.ml b/tactics/inv.ml index c99c15a45..7308b7091 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names gl = (fun id -> (tclTHEN (apply_term (mkVar id) - (List.tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) + (List.init neqns (fun _ -> Evarutil.mk_new_meta()))) reflexivity))]) gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ac783adf3..210800955 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -938,14 +938,14 @@ let descend_in_conjunctions tac exit c gl = let elim = pf_apply build_case_analysis_scheme gl ind false sort in NotADefinedRecordUseScheme elim in tclFIRST - (List.tabulate (fun i gl -> + (List.init n (fun i gl -> match make_projection (project gl) params cstr sign elim i n c with | None -> tclFAIL 0 (mt()) gl | Some (p,pt) -> tclTHENS (internal_cut id pt) [refine p; (* Might be ill-typed due to forbidden elimination. *) - tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl) n) + tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl)) gl | None -> raise Exit |