diff options
Diffstat (limited to 'lib/coq/Operators_mwords.v')
| -rw-r--r-- | lib/coq/Operators_mwords.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v index 9b38c95c..bfbf6549 100644 --- a/lib/coq/Operators_mwords.v +++ b/lib/coq/Operators_mwords.v @@ -528,7 +528,7 @@ destruct n. compute. intuition. * simpl in *. destruct (weq v w). + subst. rewrite weqb_eq; tauto. - + rewrite weqb_ne; auto. intuition. + + rewrite weqb_ne; auto. split; congruence. * destruct v. Qed. |