diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 36 |
1 files changed, 15 insertions, 21 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index aec765c..38fe27a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -849,16 +849,13 @@ Section CORRECTNESS. all: big_tac. - 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } + 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + + 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. @@ -952,22 +949,19 @@ Section CORRECTNESS. all: big_tac. - 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } + 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + + 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. (** Equality proof *) - match goal with + match goal with (* Prevents issues with evars *) | [ |- context [valueToNat ?x] ] => assert (Z.to_nat (Integers.Ptrofs.unsigned |