diff options
| author | Hugo Herbelin | 2015-08-02 21:08:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 21:45:48 +0200 |
| commit | 97fba91264669d495643f6a3de6a09790ae2a1da (patch) | |
| tree | 713f13b9c63763d20e1984e594abb449530984df | |
| parent | 47b4573a77ef88f8528c8247108eba8b04d81525 (diff) | |
Continuing 817308ab (use ltac env for terms in ltac context) + fix
of syntax in test file ltac.v.
| -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. |