diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:01:12 +0200 |
| commit | 662d6581c852496d5bb62e27893810e2514cdfbb (patch) | |
| tree | 46a22e172eb438d2de0106c846f66aa08f441bb9 /pretyping | |
| parent | 82df5a27656753f50b5f5ff7d1faa37b2ddefc49 (diff) | |
| parent | 3810a76a85a83242a739bacdfd2c8485a8e4c9da (diff) | |
Merge PR #806: closing bug 5315
Diffstat (limited to 'pretyping')
| -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 |