From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- engine/termops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index b536b0fb8..24c2c82f2 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -254,6 +254,7 @@ val clear_named_body : Id.t -> env -> env val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t +val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -- cgit v1.2.3