diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-03-18 23:35:22 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-03-19 14:17:26 -0400 |
| commit | b591ae00c3f6512c6be1469c865d4113ad33b04e (patch) | |
| tree | 5d725a5224785e3ca3a1fef674910d596fe5202f /src/Experiments/SimplyTypedArithmetic.v | |
| parent | 2ee5a1b54d1fe45f621e0f77f3446e348e4c1d19 (diff) | |
Fix for Coq <= 8.7
Diffstat (limited to 'src/Experiments/SimplyTypedArithmetic.v')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 1b58ede58..5439c1027 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -6128,9 +6128,9 @@ Section rcarry_mul. Lemma Interp_rn : Interp rn = n. Proof. reflexivity. Qed. Lemma Interp_ridxs : Interp ridxs = idxs. Proof. t_solve_interp. Qed. - Local Hint Rewrite @Interp_APP : interp_correct. - Local Hint Rewrite Interp_rs Interp_rc Interp_rn Interp_ridxs : interp_correct. - Local Hint Rewrite carry_mul_gen_correct carry_gen_correct id_gen_correct add_gen_correct sub_gen_correct opp_gen_correct encode_gen_correct zero_gen_correct one_gen_correct : interp_correct. + Hint Rewrite @Interp_APP : interp_correct. + Hint Rewrite Interp_rs Interp_rc Interp_rn Interp_ridxs : interp_correct. + Hint Rewrite carry_mul_gen_correct carry_gen_correct id_gen_correct add_gen_correct sub_gen_correct opp_gen_correct encode_gen_correct zero_gen_correct one_gen_correct : interp_correct. Local Ltac do_interp_correct := intros; repeat autorewrite with interp_correct; reflexivity. |