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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1972aee28..b1dec0fd0 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -315,6 +315,11 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let new_pure_evar_full evd evi = + let evk = new_untyped_evar () in + let evd = Evd.add evd evk evi in + (evd, evk) + let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = let newevk = new_untyped_evar() in let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in |