From ac5d50d405ad878b6899d483e64576de63d2d095 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 01:44:59 +0200
Subject: 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.
---
 vernac/comAssumption.mli | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'vernac/comAssumption.mli')

diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 32914cc11b..7c64317b70 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -9,8 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
-open Entries
 open Vernacexpr
 open Constrexpr
 open Decl_kinds
@@ -25,19 +23,13 @@ val do_assumptions
   -> (ident_decl list * constr_expr) with_coercion list
   -> bool
 
-(************************************************************************)
-(** Internal API  *)
-(************************************************************************)
-
-(** Exported for Classes *)
-
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
   :  pstate:Proof_global.t option
   -> coercion_flag
   -> assumption_kind
-  -> types in_universes_entry
+  -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> bool (** implicit *)
@@ -45,4 +37,14 @@ val declare_assumption
   -> variable CAst.t
   -> GlobRef.t * Univ.Instance.t * bool
 
+(** 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
+
 val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
-- 
cgit v1.2.3