diff options
| author | herbelin | 2007-09-01 10:35:26 +0000 |
|---|---|---|
| committer | herbelin | 2007-09-01 10:35:26 +0000 |
| commit | aae13cd8c4d76a0c1d7db42e4451c63587a1ab56 (patch) | |
| tree | 9c0a9fc128169e95922c8d35ba4f93f7c7f79ebf | |
| parent | 16d3b231355327fa6ccc65c04790fc0415d37aef (diff) | |
Suite commit 10103 (expansion des défs locales triviales dans l'étape
de "projection" lors de l'instanciation d'une evar -- fonction "real_clean")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10109 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 72f5fbf453..ddb21e838e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -467,7 +467,7 @@ let rec real_clean env isevars ev subst rhs = mkEvar (ev,args') | Var id -> (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *) - (try List.assoc t subst' + (try List.assoc (expand_var env t) subst' with Not_found -> if not rigid then t else raise (NotClean t)) | _ -> (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *) |