diff options
| author | letouzey | 2013-04-15 16:04:56 +0000 |
|---|---|---|
| committer | letouzey | 2013-04-15 16:04:56 +0000 |
| commit | 56c88d763b0cf636a740f531bd7d734426769d7d (patch) | |
| tree | 720ad9b125abc6d1d2faaf65d218e365fcd64a06 /kernel | |
| parent | 6a05c7e546a9dd2065f35b788b35e7a85866dfc8 (diff) | |
Checker: regroup all vo-related types in cic.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index c5f23ae9c4..e585e66b71 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -95,7 +95,7 @@ val mkSet : types val mkType : Univ.universe -> types -(* This defines the strategy to use for verifiying a Cast *) +(** This defines the strategy to use for verifiying a Cast *) type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast (** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the @@ -331,7 +331,7 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 Local } *) +(** {6 Local context} *) (** A {e declaration} has the form [(name,body,type)]. It is either an {e assumption} if [body=None] or a {e definition} if [body=Some actualbody]. It is referred by {e name} if [na] is an |