From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- engine/termops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 0dd5d96fb..fe6dfb0ce 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -250,7 +250,7 @@ val clear_named_body : Id.t -> env -> env val global_vars : env -> Evd.evar_map -> constr -> Id.t list val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option +val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -259,7 +259,7 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses +val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool -- cgit v1.2.3