diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-04 16:51:23 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-04 16:51:23 +0000 |
| commit | d91e0f86111718bc3146a6925d6f39c53ee990f1 (patch) | |
| tree | d81de6d2eded5c99e1bfda2fcb009f8120bed4d8 /kernel/context.mli | |
| parent | 9fd3b0c4f47fd83ce2ded3864fe2074463151aca (diff) | |
Removing useless casts between arrays and lists.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 79ddbe49b..ad6d645cd 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -75,7 +75,7 @@ val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a (** {6 Section-related auxiliary functions } *) -val instance_from_named_context : named_context -> Constr.t array +val instance_from_named_context : named_context -> Constr.t list (** {6 ... } *) (** Signatures of ordered optionally named variables, intended to be |