remove old pipeline

2 files changed, 0 insertions, 67 deletions

diff --git a/src/Compilers/Named/PositiveContext/Defaults.v b/src/Compilers/Named/PositiveContext/Defaults.v
deleted file mode 100644
index 066de61cb..000000000
--- a/src/Compilers/Named/PositiveContext/Defaults.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.PositiveContext.
-Require Import Crypto.Compilers.Named.CountLets.
-Require Import Crypto.Compilers.CountLets.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
-  Definition default_names_forf {var} (dummy : forall t, var t) {t} (e : exprf base_type_code op (var:=var) t) : list positive
-    := map BinPos.Pos.of_succ_nat (seq 0 (count_let_bindersf dummy e)).
-  Definition default_names_for {var} (dummy : forall t, var t) {t} (e : expr base_type_code op (var:=var) t) : list positive
-    := map BinPos.Pos.of_succ_nat (seq 0 (count_binders dummy e)).
-  Definition DefaultNamesFor {t} (e : Expr base_type_code op t) : list positive
-    := map BinPos.Pos.of_succ_nat (seq 0 (CountBinders e)).
-End language.
-
-Module Named.
-  Section language.
-    Context {base_type_code : Type}
-            {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
-    Definition default_names_forf {Name} {t} (e : Named.exprf base_type_code op Name t) : list positive
-      := map BinPos.Pos.of_succ_nat (seq 0 (Named.CountLets.count_let_bindersf e)).
-    Definition default_names_for {Name} {t} (e : Named.expr base_type_code op Name t) : list positive
-      := map BinPos.Pos.of_succ_nat (seq 0 (Named.CountLets.count_binders e)).
-  End language.
-End Named.
diff --git a/src/Compilers/Named/PositiveContext/DefaultsProperties.v b/src/Compilers/Named/PositiveContext/DefaultsProperties.v
deleted file mode 100644
index 2b46de136..000000000
--- a/src/Compilers/Named/PositiveContext/DefaultsProperties.v
+++ /dev/null
@@ -1,38 +0,0 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.PositiveContext.
-Require Import Crypto.Compilers.CountLets.
-Require Import Crypto.Compilers.Named.NameUtil.
-Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
-Require Import Crypto.Util.ListUtil.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.Tactics.DestructHead.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
-
-  Lemma name_list_unique_map_pos_of_succ_nat_seq a b
-    : name_list_unique (map BinPos.Pos.of_succ_nat (seq a b)).
-  Proof using Type.
-    unfold name_list_unique, oname_list_unique, mname_list_unique.
-    intros k n.
-    rewrite !map_map, firstn_map, skipn_map, firstn_seq, skipn_seq.
-    rewrite !in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst.
-    match goal with H : _ |- _ => apply Pnat.SuccNat2Pos.inj in H end; subst.
-    rewrite in_seq in *.
-    omega *.
-  Qed.
-
-  Lemma name_list_unique_default_names_forf {var dummy t e}
-    : name_list_unique (@default_names_forf base_type_code op var dummy t e).
-  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
-  Lemma name_list_unique_default_names_for {var dummy t e}
-    : name_list_unique (@default_names_for base_type_code op var dummy t e).
-  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
-  Lemma name_list_unique_DefaultNamesFor {t e}
-    : name_list_unique (@DefaultNamesFor base_type_code op t e).
-  Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed.
-End language.