diff options
Diffstat (limited to 'src/RewriterWf1.v')
-rw-r--r-- | src/RewriterWf1.v | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index 19ea1e9e7..2b18d01d0 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -302,20 +302,6 @@ Module Compilers. Ltac add_var_types_cps_id := cps_id_with_option (@add_var_types_cps_id _ _ _ _ _). - Lemma unify_extracted_cps_id {pt et T k} - : @pattern.base.unify_extracted_cps pt et T k = k (@pattern.base.unify_extracted_cps pt et _ id). - Proof using Type. - revert et T k; induction pt, et; cbn [pattern.base.unify_extracted_cps]; cbv [id] in *; intros; - repeat first [ reflexivity - | progress inversion_option - | progress subst - | break_innermost_match_step - | rewrite_hyp !* ]. - Qed. - - Ltac unify_extracted_cps_id := - cps_id_with_option (@unify_extracted_cps_id _ _ _ _). - Lemma mem_collect_vars_subst_Some_find {x t evm t'} (Hmem : PositiveSet.mem x (pattern.base.collect_vars t) = true) (H : pattern.base.subst t evm = Some t') @@ -403,21 +389,6 @@ Module Compilers. Ltac add_var_types_cps_id := cps_id_with_option (@add_var_types_cps_id _ _ _ _ _). - Lemma unify_extracted_cps_id {pt et T k} - : @pattern.type.unify_extracted_cps pt et T k = k (@pattern.type.unify_extracted_cps pt et _ id). - Proof using Type. - revert et T k; induction pt, et; cbn [pattern.type.unify_extracted_cps]; cbv [id] in *; intros; - repeat first [ reflexivity - | progress inversion_option - | progress subst - | apply base.unify_extracted_cps_id - | break_innermost_match_step - | rewrite_hyp !* ]. - Qed. - - Ltac unify_extracted_cps_id := - cps_id_with_option (@unify_extracted_cps_id _ _ _ _). - Local Ltac t_subst_eq_iff := repeat first [ progress apply conj | progress cbv [option_map Option.bind] in * |