diff options
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a212735c04..2858a5c1fe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -297,13 +297,14 @@ let protected_get_type_of env sigma c = (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") -let pretype_id pretype loc env evdref lvar id = +let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> + let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -433,7 +434,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GVar (loc, id) -> 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) + (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon | GEvar (loc, id, inst) -> diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 952f35bc35..f9df021dc2 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -304,5 +304,5 @@ Abort. Goal True. let x := ipattern:y in assert (forall x y, x = y + 0). intro. -destruct y. (* Check that the name is y here *). +destruct y. (* Check that the name is y here *) Abort. |