diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-21 18:51:28 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-21 18:51:28 -0500 |
| commit | 3c4ff8fe8d2154addcf440690d315c58a529c1f6 (patch) | |
| tree | d30a09c920c0be970356c2ac71c2774012b00972 /src | |
| parent | c83cb07f1477de33ce9eb43eea6a4f2720a94763 (diff) | |
Fix a missing qualification
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/WordUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index d36292f95..0e3f6a168 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1220,7 +1220,7 @@ Proof. repeat first [ progress simpl | intro | congruence - | exists eq_refl + | exists Logic.eq_refl | progress destruct_head ex | progress destruct_head bool | progress subst |