diff options
| author | Arnaud Spiwack | 2014-09-15 14:42:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-15 15:44:11 +0200 |
| commit | 7ec7714aa7649fc1bae463f4200fa8c16729026a (patch) | |
| tree | 4da4fc06959bd438ae4c6aa111a7176611865628 | |
| parent | 006c487f8af220cf8a374bc38d06c3d58fe4335b (diff) | |
Fix: when interpreting a identifier in pretying, use the Ltac identifier substitution at the right place.
I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d348b5eeb0..dfb6f80d9c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -275,6 +275,10 @@ let pretype_id pretype loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try + let id = + try Id.Map.find id lvar.ltac_idents + with Not_found -> id + in let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -411,10 +415,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var tycon | GVar (loc, id) -> - let id = - try Id.Map.find id lvar.ltac_idents - with Not_found -> id - in inh_conv_coerce_to_tycon loc env evdref (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id) tycon |