Functionalize env in type classes

I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.

1 files changed, 12 insertions, 10 deletions

diff --git a/vernac/classes.mli b/vernac/classes.mli
index 73e4b024ef..e7f90ff306 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,6 +22,12 @@ val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
 
 (** Instance declaration *)
 
+val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
+                       hint_info option -> bool -> GlobRef.t -> unit
+(** Declares the given global reference as an instance of its type.
+    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
+    when said type is not a registered type class. *)
+
 val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
@@ -64,6 +70,12 @@ val declare_new_instance :
   Hints.hint_info_expr ->
   unit
 
+(** {6 Low level interface used by Add Morphism, do not use } *)
+val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
+val add_instance : instance -> unit
+
+val add_class : env -> Evd.evar_map -> typeclass -> unit
+
 (** Setting opacity *)
 
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -71,13 +83,3 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 (** For generation on names based on classes only *)
 
 val id_of_class : typeclass -> Id.t
-
-(** Context command *)
-
-(** returns [false] if, for lack of section, it declares an assumption
-    (unless in a module type). *)
-val context
-  :  pstate:Proof_global.t option
-  -> Decl_kinds.polymorphic
-  -> local_binder_expr list
-  -> bool