diff options
Diffstat (limited to 'src/Compilers/Z')
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierWf.v | 11 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 2 |
2 files changed, 9 insertions, 4 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index ba5dd39cd..56dda81ab 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -115,7 +115,8 @@ Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2} end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; - try invert_one_expr e2; intros; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); intros; repeat first [ fin_t | progress simpl in * | progress intros @@ -157,7 +158,9 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); + intros; break_innermost_match; intros; try exact I; repeat first [ pret_step | pose_wff_base | break_t_step @@ -206,7 +209,9 @@ Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 end. Proof. invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in + invert_one_expr e2); + intros; break_innermost_match; intros; try exact I; repeat first [ pret_step | pose_wff_base | pose_wff_prod diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index dc29fe654..882cbde3a 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -288,7 +288,7 @@ Module Import Bounds. := interp_flat_type_rel_pointwise (@is_bounded_by'). Local Arguments interp_base_type !_ / . - Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. + Global Instance dec_eq_interp_flat_type : forall {T}, DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. Proof. induction T; destruct_head base_type; simpl; exact _. Defined. |