diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e38b9a6e69..6d01ea00c9 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -808,7 +808,8 @@ let refresh_hypinfo env sigma hypinfo = else () let unify_eqn env sigma hypinfo t = - try + if isEvar t then None + else try let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in let env', prf, c1, c2, car, rel = let left = if l2r then c1 else c2 in |