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/functional_principles_proofs.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/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0796930fca..3505c4d9b8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -371,7 +371,7 @@ let is_property ptes_info t_x full_type_of_hyp = if isApp t_x then let pte,args = destApp t_x in - if isVar pte && array_for_all closed0 args + if isVar pte && Array.for_all closed0 args then try let info = Idmap.find (destVar pte) ptes_info in @@ -1415,11 +1415,11 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = tclFIRST (List.map Equality.rewriteRL eqs ) in let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in - let f_app = array_last (snd (destApp hrec_concl)) in + let f_app = Array.last (snd (destApp hrec_concl)) in let f = (fst (destApp f_app)) in let rec backtrack : tactic = fun g -> - let f_app = array_last (snd (destApp (pf_concl g))) in + let f_app = Array.last (snd (destApp (pf_concl g))) in match kind_of_term f_app with | App(f',_) when eq_constr f' f -> tclIDTAC g | _ -> tclTHEN rewrite backtrack g @@ -1658,7 +1658,7 @@ let prove_principle_for_gen (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in - array_last args + Array.last args in let body_info rec_hyps = { |