diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-22 16:12:08 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-22 16:12:08 -0400 |
| commit | 2e145ec01ca8f6d97a58f1e54b487824b8595951 (patch) | |
| tree | 7ba7de3ac63f89144212836b67648bbff517deae /src/Assembly/Conversions.v | |
| parent | 7a0ca3b4172584368a3d83053db77f287f3d5ddd (diff) | |
More Coq 8.4 fixes
Diffstat (limited to 'src/Assembly/Conversions.v')
| -rw-r--r-- | src/Assembly/Conversions.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index b6844ebd0..c24cf618f 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -284,7 +284,7 @@ Module LLConversions. Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None. Proof. intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV; - kill_dec; simpl; kill_dec; simpl; try abstract (intro Z; inversion Z); + break_match; simpl; try break_match; simpl; try abstract (intro Z; inversion Z); pose proof (Npow2_gt0 n); simpl in *; nomega. Qed. @@ -363,7 +363,7 @@ Module LLConversions. kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *) + unfold bcheck, getBounds in *. - replace (interp_binop op _ _) + replace (interp_binop op (interp_arg x) (interp_arg y)) with (varBoundedToZ (n := n) (opBounded op (interp_arg' boundVarInterp (convertArg _ x)) (interp_arg' boundVarInterp (convertArg _ y)))). |