From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 toplevel/classes.mli | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'toplevel/classes.mli')

diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 24c51b31..d2cb788e 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Context
 open Environ
 open Constrexpr
 open Typeclasses
@@ -15,24 +14,25 @@ open Libnames
 
 (** Errors *)
 
-val mismatched_params : env -> constr_expr list -> rel_context -> 'a
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
 
-val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> int option -> unit
-(** globality, reference, priority *)
+val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+(** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  int option -> (** priority *)
+  Vernacexpr.hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
+  Id.t Loc.located list option ->
   bool -> (* polymorphic *)
-  Univ.universe_context_set -> (* Universes *)
+  Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
@@ -40,6 +40,7 @@ val declare_instance_constant :
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
+  ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
   local_binder list ->
   typeclass_constraint ->
@@ -47,7 +48,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
-  int option ->
+  Vernacexpr.hint_info_expr ->
   Id.t
 
 (** Setting opacity *)
-- 
cgit v1.2.3