From bbde815f8108f4641f5411d03f7a88096cc2221b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 24 May 2017 21:55:21 +0200 Subject: Support for using type information to infer more precise evar sources. This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted). --- engine/evarutil.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index fcc435a2e..496ec5bc4 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma + ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) -- cgit v1.2.3