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

---
 toplevel/record.mli | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'toplevel/record.mli')

diff --git a/toplevel/record.mli b/toplevel/record.mli
index 44b34550..45670f1f 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  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: record.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Term
 open Sign
@@ -16,28 +13,27 @@ open Vernacexpr
 open Topconstr
 open Impargs
 open Libnames
-(*i*)
 
-(* [declare_projections ref name coers params fields] declare projections of
+(** [declare_projections ref name coers params fields] declare projections of
    record [ref] (if allowed) using the given [name] as argument, and put them
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
-  bool list -> manual_explicitation list list -> rel_context ->
+  coercion_flag list -> manual_explicitation list list -> rel_context ->
   (name * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
-  bool (*infer?*) -> identifier -> identifier ->
-  manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
-  Impargs.manual_explicitation list list -> rel_context -> (* fields *)
+  bool (**infer?*) -> identifier -> identifier ->
+  manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+  Impargs.manual_explicitation list list -> rel_context -> (** fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
-  bool -> (* coercion? *)
-  bool list -> (* field coercions *)
+  bool -> (** coercion? *)
+  bool list -> (** field coercions *)
   Evd.evar_map ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion with_notation) list *
+  inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
+  (local_decl_expr with_instance with_priority with_notation) list *
   identifier * constr_expr option -> global_reference
-- 
cgit v1.2.3