diff options
| author | Brian Campbell | 2020-09-30 17:25:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-09-30 17:26:09 +0100 |
| commit | ce94aec9d6604b41217529525b7a73850c530e7b (patch) | |
| tree | d3311c56f30006e306d13b023e3e03ff39151cd8 | |
| parent | 36cd0d8a7a146f8d51ef920212be768428680dac (diff) | |
Tweak Coq proof to avoid incompatibility with Iris
(in the previous proof script the intuition tactic found a strange proof
involving a type-level dependent pair that imposed an unnecessary
universe constraint, this doesn't)
| -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. |