diff options
| author | ppedrot | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /plugins/funind/invfun.ml | |
| parent | 6eaff635db797d1f9225b22196832c1bb76c0d94 (diff) | |
As r15801: putting everything from Util.array_* to CArray.*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1d1089a549..d8255e8342 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -358,7 +358,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | App(eq,args), App(graph',_) when (eq_constr eq eq_ind) && - array_exists (eq_constr graph') graphs_constr -> + Array.exists (eq_constr graph') graphs_constr -> (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) ::acc) | _ -> mkVar hid :: acc @@ -599,7 +599,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | App(eq,args), App(graph',_) when (eq_constr eq eq_ind) && - array_exists (eq_constr graph') graphs_constr -> + Array.exists (eq_constr graph') graphs_constr -> ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) ::args.(2)::acc) | _ -> mkVar hid :: acc @@ -1029,7 +1029,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g try let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = - Util.array_map2_i + Util.Array.map2_i (fun i f_constr graph -> let const_of_f = destConst f_constr in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = @@ -1056,7 +1056,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,GType None) funs)) + (make_scheme (Array.map_to_list (fun const -> const,GType None) funs)) ) in let proving_tac = @@ -1083,7 +1083,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g ) funs; let lemmas_types_infos = - Util.array_map2_i + Util.Array.map2_i (fun i f_constr graph -> let const_of_f = destConst f_constr in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = @@ -1169,7 +1169,7 @@ let revert_graph kn post_tac hid g = match info.completeness_lemma with | None -> tclIDTAC g | Some f_complete -> - let f_args,res = array_chop (Array.length args - 1) args in + let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; |