From 7ec7714aa7649fc1bae463f4200fa8c16729026a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 15 Sep 2014 14:42:05 +0200
Subject: 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.---
 pretyping/pretyping.ml | 8 ++++----
 1 file 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
-- 
cgit v1.2.3