diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-26 19:50:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-26 23:32:04 +0200 |
| commit | f52826877059858fb3fcd4314c629ed63d90a042 (patch) | |
| tree | 4142e0e4cb4850230e2a79cabc8e1c16bba1e4c9 /pretyping/evarutil.mli | |
| parent | 39b2c31fed01073a4308e2e85d8a53ccecde73e7 (diff) | |
Hardening the API of evarmaps.
The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f1d94b0a4..76d67c748 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -252,4 +252,3 @@ 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 |