From 25c3428cebabf4c0cf19aa20cf6857560052e849 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 31 Jan 2019 18:52:33 -0500 Subject: Uncps unify_extracted We never used the cps form, and this form is easier to read. --- src/RewriterWf1.v | 29 ----------------------------- 1 file changed, 29 deletions(-) (limited to 'src/RewriterWf1.v') 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 * -- cgit v1.2.3