diff options
Diffstat (limited to 'pretyping/globEnv.ml')
| -rw-r--r-- | pretyping/globEnv.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 57bedf1ee9..12788e5ec5 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -107,6 +107,11 @@ let e_new_evar env evdref ?src ?naming typ = evdref := sigma; e +let e_new_type_evar env evdref ~src = + let (evd', s) = Evd.new_sort_variable Evd.univ_flexible_alg !evdref in + evdref := evd'; + e_new_evar env evdref ~src (EConstr.mkSort s) + let hide_variable env expansion id = let lvar = env.lvar in if Id.Map.mem id lvar.ltac_genargs then |