diff options
| author |  Julien Forest <forest@ensiie.fr> | 2017-06-16 16:45:47 +0200 |
|---|---|---|
| committer | Julien Forest <forest@ensiie.fr> | 2017-07-29 10:28:07 +0200 |
| commit | 3810a76a85a83242a739bacdfd2c8485a8e4c9da (patch) | |
| tree | f9c3b50a86f44c06e16aa74907e4050c5a609ecf /pretyping/pretyping.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
closing bug 5315
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bfc6bf5cf..b4d87dfdb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1136,8 +1136,13 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in - { utj_val = v; - utj_type = s } + (* Correction of bug #5315 : we need to define an evar for *all* holes *) + let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in + let ev,_ = destEvar !evdref evkt in + evdref := Evd.define ev (to_constr !evdref v) !evdref; + (* End of correction of bug #5315 *) + { utj_val = v; + utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in |