From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 library/decl_kinds.mli | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

(limited to 'library/decl_kinds.mli')

diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 38e83b1e..88ef763c 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -1,24 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Libnames
 
-(* Informal mathematical status of declarations *)
+(** Informal mathematical status of declarations *)
 
 type locality =
   | Local
   | Global
 
-type boxed_flag = bool
-
 type theorem_kind =
   | Theorem
   | Lemma
@@ -44,7 +40,7 @@ type definition_object_kind =
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
-(* [assumption_kind]
+(** [assumption_kind]
 
                 |  Local      | Global
    ------------------------------------
@@ -54,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 *)
 type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality * boxed_flag * definition_object_kind
+type definition_kind = locality * definition_object_kind
 
-(* Kinds used in proofs *)
+(** Kinds used in proofs *)
 
 type goal_object_kind =
   | DefinitionBody of definition_object_kind
@@ -64,31 +60,31 @@ type goal_object_kind =
 
 type goal_kind = locality * goal_object_kind
 
-(* Kinds used in library *)
+(** Kinds used in library *)
 
 type logical_kind =
   | IsAssumption of assumption_object_kind
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
 
-(* Utils *)
+(** Utils *)
 
 val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 val string_of_theorem_kind : theorem_kind -> string
 val string_of_definition_kind :
-  locality * boxed_flag * definition_object_kind -> string
+  locality * definition_object_kind -> string
 
-(* About locality *)
+(** About locality *)
 
 val strength_of_global : global_reference -> locality
 val string_of_strength : locality -> string
 
-(* About recursive power of type declarations *)
+(** About recursive power of type declarations *)
 
 type recursivity_kind =
-  | Finite (* = inductive *)
-  | CoFinite (* = coinductive *)
-  | BiFinite (* = non-recursive, like in "Record" definitions *)
+  | Finite (** = inductive *)
+  | CoFinite (** = coinductive *)
+  | BiFinite (** = non-recursive, like in "Record" definitions *)
 
-(* helper, converts to "finiteness flag" booleans *)
+(** helper, converts to "finiteness flag" booleans *)
 val recursivity_flag_of_kind : recursivity_kind -> bool
-- 
cgit v1.2.3