diff options
| -rw-r--r-- | src/Reflection/BoundByCast.v | 4 | ||||
| -rw-r--r-- | src/Reflection/EtaWf.v | 8 |
2 files changed, 7 insertions, 5 deletions
diff --git a/src/Reflection/BoundByCast.v b/src/Reflection/BoundByCast.v index 09bdc207e..89170ec2f 100644 --- a/src/Reflection/BoundByCast.v +++ b/src/Reflection/BoundByCast.v @@ -30,8 +30,8 @@ Section language. Definition Boundify {t1} (e1 : Expr t1) args2 : Expr _ := ExprEta - (InlineConstGen - (@push_cast _ _ _ base_type_bl_transparent base_type_leb Cast is_cast is_const) + (InlineCast + _ base_type_bl_transparent base_type_leb Cast is_cast is_const (Linearize (SmartBound _ diff --git a/src/Reflection/EtaWf.v b/src/Reflection/EtaWf.v index fd2adaa8a..a9e41e3eb 100644 --- a/src/Reflection/EtaWf.v +++ b/src/Reflection/EtaWf.v @@ -93,7 +93,7 @@ Section language. Qed. End with_var. - Lemma WfExprEtaGen + Lemma Wf_ExprEtaGen (eta : forall {A B}, A * B -> A * B) (eq_eta : forall A B x, @eta A B x = x) {t e} @@ -104,16 +104,18 @@ Section language. symmetry; apply wff_exprf_eta_gen; auto. Qed. - Lemma WfExprEta + Lemma Wf_ExprEta {t e} : Wf (ExprEta e) <-> @Wf base_type_code op t e. Proof. unfold Wf; setoid_rewrite wf_expr_eta; reflexivity. Qed. - Lemma WfExprEta' + Lemma Wf_ExprEta' {t e} : Wf (ExprEta' e) <-> @Wf base_type_code op t e. Proof. unfold Wf; setoid_rewrite wf_expr_eta'; reflexivity. Qed. End language. + +Hint Resolve <- Wf_ExprEta Wf_ExprEta' : wf. |