diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-31 18:52:33 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-01 23:40:21 -0500 |
| commit | 25c3428cebabf4c0cf19aa20cf6857560052e849 (patch) | |
| tree | e07a8d9186c4d3c43c072b9122eed821be6aa0be /src/RewriterWf1.v | |
| parent | 014c627a93f09c2867e76e35837eb8cb64f98384 (diff) | |
Uncps unify_extracted
We never used the cps form, and this form is easier to read.
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 * |