diff options
| author | Hugo Herbelin | 2018-04-13 18:01:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | bb78a36d77ff37ba9fc11d6db914ee4bc71e3e2e (patch) | |
| tree | 744607c59fa472a2de30e9bf41f90807a10f2790 /pretyping/globEnv.ml | |
| parent | 9371ab87e8bac42216f882ed8f00e6fba9dc6eb0 (diff) | |
Relying on the precomputation of the renaming also for new_evar_type.
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 |