diff options
| -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" *) |