diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 92a3984ba..49036798e 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -243,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 |