diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /plugins/quote | |
| 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/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 8dbb75cdc..311ab3081 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,7 +211,7 @@ let compute_rhs bodyi index_of_f = let rec aux c = match kind_of_term c with | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) -> - let i = destRel (array_last args) in + let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args) @@ -301,7 +301,7 @@ let rec closed_under cset t = (ConstrSet.mem t cset) or (match (kind_of_term t) with | Cast(c,_,_) -> closed_under cset c - | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l + | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l | _ -> false) (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete @@ -362,7 +362,7 @@ let path_of_int n = let rec subterm gl (t : constr) (t' : constr) = (pf_conv_x gl t t') or (match (kind_of_term t) with - | App (f,args) -> array_exists (fun t -> subterm gl t t') args + | App (f,args) -> Array.exists (fun t -> subterm gl t t') args | Cast(t,_,_) -> (subterm gl t t') | _ -> false) |