1 files changed, 20 insertions, 28 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 97b363c2..0a351d3c 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -1,23 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Decl_kinds
-open Term
-open Sign
+open Context
 open Evd
 open Environ
-open Nametab
-open Mod_subst
-open Topconstr
-open Util
+open Constrexpr
 open Typeclasses
-open Implicit_quantifiers
 open Libnames
 
 (** Errors *)
@@ -26,36 +20,36 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
-(** Post-hoc class declaration. *)
-
-val declare_class : reference -> unit
-
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> unit
+val existing_instance : bool -> reference -> int option -> unit
+(** globality, reference, priority *)
 
 val declare_instance_constant :
   typeclass ->
   int option -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
-  ?hook:(Libnames.global_reference -> unit) ->
-  identifier -> (** name *)
-  Term.constr -> (** body *)
+  ?hook:(Globnames.global_reference -> unit) ->
+  Id.t -> (** name *)
+  bool -> (* polymorphic *)
+  Univ.universe_context -> (* Universes *)
+  Constr.t -> (** body *)
   Term.types -> (** type *)
-  Names.identifier
+  Names.Id.t
 
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
+  Decl_kinds.polymorphic ->
   local_binder list ->
   typeclass_constraint ->
-  constr_expr option ->
+  (bool * constr_expr) option ->
   ?generalize:bool ->
-  ?tac:Proof_type.tactic  ->
-  ?hook:(Libnames.global_reference -> unit) ->
+  ?tac:unit Proofview.tactic  ->
+  ?hook:(Globnames.global_reference -> unit) ->
   int option ->
-  identifier
+  Id.t
 
 (** Setting opacity *)
 
@@ -63,12 +57,10 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 
 (** For generation on names based on classes only *)
 
-val id_of_class : typeclass -> identifier
+val id_of_class : typeclass -> Id.t
 
 (** Context command *)
 
-val context : local_binder list -> unit
-
-(** Forward ref for refine *)
-
-val refine_ref : (open_constr -> Proof_type.tactic) ref
+(** returns [false] if, for lack of section, it declares an assumption
+    (unless in a module type). *)
+val context : Decl_kinds.polymorphic -> local_binder list -> bool