diff options
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 |