From 56c88d763b0cf636a740f531bd7d734426769d7d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Apr 2013 16:04:56 +0000
Subject: 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
---
 kernel/term.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3