diff options
Diffstat (limited to 'vernac/retrieveObl.ml')
| -rw-r--r-- | vernac/retrieveObl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml index c529972b8d..b8564037e0 100644 --- a/vernac/retrieveObl.ml +++ b/vernac/retrieveObl.ml @@ -72,7 +72,7 @@ let subst_evar_constr evm evs n idf t = *) let args = let n = match chop with None -> 0 | Some c -> c in - let l, r = CList.chop n (List.rev (Array.to_list args)) in + let l, r = CList.chop n (List.rev args) in List.rev r in let args = |