diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-19 12:08:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-24 18:50:39 +0100 |
| commit | f7b29094fe7cc13ea475447bd30d9a8b942f0fef (patch) | |
| tree | b1533a863e91a2650e2706b4955337f526249b36 /pretyping/evarutil.mli | |
| parent | fc6d0fb650f57a764af6fe9be44677a69be11980 (diff) | |
[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).
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 7 |
1 files changed, 7 insertions, 0 deletions
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 |