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

---
 kernel/sign.mli | 36 +++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 17 deletions(-)

(limited to 'kernel/sign.mli')

diff --git a/kernel/sign.mli b/kernel/sign.mli
index 35e49003..074139c9 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,19 +1,15 @@
 (************************************************************************)
 (*  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        *)
 (************************************************************************)
 
-(*i $Id: sign.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Term
-(*i*)
 
-(*s Signatures of ordered named declarations *)
+(** {6 Signatures of ordered named declarations } *)
 
 type named_context = named_declaration list
 type section_context = named_context
@@ -24,39 +20,45 @@ val vars_of_named_context : named_context -> identifier list
 
 val lookup_named : identifier -> named_context -> named_declaration
 
-(* number of declarations *)
+(** number of declarations *)
 val named_context_length : named_context -> int
 
-(*s Recurrence on [named_context]: older declarations processed first *)
+(** named context equality *)
+val named_context_equal : named_context -> named_context -> bool
+
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
 val fold_named_context :
   (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
 val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
 
-(*s Section-related auxiliary functions *)
+(** {6 Section-related auxiliary functions } *)
 val instance_from_named_context : named_context -> constr array
 
-(*s Signatures of ordered optionally named variables, intended to be
+(** {6 ... } *)
+(** Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
 val push_named_to_rel_context : named_context -> rel_context -> rel_context
 
-(*s Recurrence on [rel_context]: older declarations processed first *)
+(** {6 Recurrence on [rel_context]: older declarations processed first } *)
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
 val fold_rel_context_reverse :
   ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
 
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
 val map_named_context : (constr -> constr) -> named_context -> named_context
 
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
 val iter_rel_context : (constr -> unit) -> rel_context -> unit
 
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
 val iter_named_context : (constr -> unit) -> named_context -> unit
-- 
cgit v1.2.3