From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- vernac/comAssumption.mli | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'vernac/comAssumption.mli') diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 56e32437..56932360 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Globnames open Vernacexpr open Constrexpr open Decl_kinds @@ -19,7 +18,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool + Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) @@ -31,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> - Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t -> - global_reference * Univ.Instance.t * bool + UnivNames.universe_binders -> Impargs.manual_implicits -> + bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> + GlobRef.t * Univ.Instance.t * bool -- cgit v1.2.3