diff options
| author | herbelin | 2005-02-02 19:07:56 +0000 |
|---|---|---|
| committer | herbelin | 2005-02-02 19:07:56 +0000 |
| commit | 708b76785e9354565de5445749e81bb680ed6098 (patch) | |
| tree | f652864eb229fdf40b98cdb56b1d62b73b84a8e5 | |
| parent | 5ec7ad5cd4ef0660b064faf0a67e47c17e908d93 (diff) | |
Correction de la précédence des contexts de variables rel, ltac et var
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8389da9b3f..bc6294d764 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -198,13 +198,13 @@ let strip_meta id = (* For Grammar v7 compatibility *) let pretype_id loc env (lvar,unbndltacvars) id = let id = strip_meta id in (* May happen in tactics defined by Grammar *) try - List.assoc id lvar - with Not_found -> - try let (n,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = type_app (lift n) typ } with Not_found -> try + List.assoc id lvar + with Not_found -> + try let (_,_,typ) = lookup_named id env in { uj_val = mkVar id; uj_type = typ } with Not_found -> |