From f7b29094fe7cc13ea475447bd30d9a8b942f0fef Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 19 Feb 2015 12:08:51 +0100 Subject: [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is progress. Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far. Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it). Fixes bugs (one reported directly on coqdev, and #3412). --- pretyping/evarutil.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'pretyping/evarutil.mli') diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f89266a60..92a3984ba 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr +(** {6 Term manipulation up to instantiation} *) + +(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] + as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the + value of [e] in [sigma] is (recursively) used. *) +val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds -- cgit v1.2.3