diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /pretyping/evarutil.mli | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'pretyping/evarutil.mli')
-rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f89266a6..49036798 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 @@ -236,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> val subterm_source : existential_key -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located + +val meta_counter_summary_name : string +val evar_counter_summary_name : string |