diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 14:03:45 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 14:03:45 +0000 |
| commit | c14ccd1b8a3855d4eb369be311d4b36a355e46c1 (patch) | |
| tree | 200520406e15532a90f57d400a414a153c4c83b4 /pretyping/evarutil.mli | |
| parent | 98c3d8f7b81a649906ddf4baf1b123cec66dc5e4 (diff) | |
Removing almost all new_untyped_evar, and a bunch of Evd.add.
Ultimately all evars should be created with respect to a given
evar map, instead of using a global counter.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7d917f15b..0d482e9b0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -36,6 +36,8 @@ val new_pure_evar : evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * evar +val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar + (** the same with side-effects *) val e_new_evar : evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> |