diff options
| author | Pierre-Marie Pédrot | 2018-09-26 14:03:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-26 14:03:35 +0200 |
| commit | 871c694e5395e85296f4c61ba4039f04704b20b3 (patch) | |
| tree | 7f61099c11a30aa4fa82810fd7949d5ffb1a7bc4 /pretyping/pretyping.ml | |
| parent | 8292c485bde7911bf8a4d626faf9292ba0016e97 (diff) | |
| parent | 8d1a5297d55eb0cd02695c81f6dea7aef6f62d31 (diff) | |
Merge PR #7309: Made names of existential variables interpretable as Ltac variables.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3aa90fbcf..a4c2cb2352 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -480,6 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref | GEvar (id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) + let id = interp_ltac_id env id in let evk = try Evd.evar_key id !evdref with Not_found -> @@ -499,6 +500,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> + let open Namegen in + let naming = match naming with + | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id) + | IntroAnonymous -> IntroAnonymous + | IntroFresh id -> IntroFresh (interp_ltac_id env id) in let ty = match tycon with | Some ty -> ty |