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/classes.mli | 46 ++++++++++++++++++++--------------------------
 1 file changed, 20 insertions(+), 26 deletions(-)

(limited to 'toplevel/classes.mli')

diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 69e4dd8b..68a93a74 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.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: classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Decl_kinds
 open Term
@@ -22,59 +19,56 @@ open Util
 open Typeclasses
 open Implicit_quantifiers
 open Libnames
-(*i*)
 
-(* Errors *)
+(** Errors *)
 
 val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
-(* Post-hoc class declaration. *)
+(** Post-hoc class declaration. *)
 
 val declare_class : reference -> unit
 
-(* Instance declaration *)
+(** Instance declaration *)
 
-val declare_instance : bool -> reference -> unit
+val existing_instance : bool -> reference -> unit
 
 val declare_instance_constant :
   typeclass ->
-  int option -> (* priority *)
-  bool -> (* globality *)
-  Impargs.manual_explicitation list -> (* implicits *)
+  int option -> (** priority *)
+  bool -> (** globality *)
+  Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Libnames.global_reference -> unit) ->
-  identifier -> (* name *)
-  Term.constr -> (* body *)
-  Term.types -> (* type *)
+  identifier -> (** name *)
+  Term.constr -> (** body *)
+  Term.types -> (** type *)
   Names.identifier
 
 val new_instance :
-  ?abstract:bool -> (* Not abstract by default. *)
-  ?global:bool -> (* Not global by default. *)
+  ?abstract:bool -> (** Not abstract by default. *)
+  ?global:bool -> (** Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
-  constr_expr ->
+  constr_expr option ->
   ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
   ?hook:(Libnames.global_reference -> unit) ->
   int option ->
   identifier
 
-(* Setting opacity *)
+(** Setting opacity *)
 
-val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
-(* For generation on names based on classes only *)
+(** For generation on names based on classes only *)
 
 val id_of_class : typeclass -> identifier
 
-(* Context command *)
+(** Context command *)
 
-val context : ?hook:(Libnames.global_reference -> unit) ->
-  local_binder list -> unit
+val context : local_binder list -> unit
 
-(* Forward ref for refine *)
+(** Forward ref for refine *)
 
 val refine_ref : (open_constr -> Proof_type.tactic) ref
-
-- 
cgit v1.2.3