diff options
author | Andres Erbsen <andreser@mit.edu> | 2019-01-08 04:21:38 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2019-01-09 22:49:02 -0500 |
commit | 3ca227f1137e6a3b65bc33f5689e1c230d591595 (patch) | |
tree | e1e5a2dd2a2f34f239d3276227ddbdc69eeeb667 /src/Arithmetic/Saturated/FreezeUnfolder.v | |
parent | 3ec21c64b3682465ca8e159a187689b207c71de4 (diff) |
remove old pipeline
Diffstat (limited to 'src/Arithmetic/Saturated/FreezeUnfolder.v')
-rw-r--r-- | src/Arithmetic/Saturated/FreezeUnfolder.v | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/src/Arithmetic/Saturated/FreezeUnfolder.v b/src/Arithmetic/Saturated/FreezeUnfolder.v deleted file mode 100644 index bae1a87f3..000000000 --- a/src/Arithmetic/Saturated/FreezeUnfolder.v +++ /dev/null @@ -1,27 +0,0 @@ -Require Import Crypto.Arithmetic.CoreUnfolder. -Require Import Crypto.Arithmetic.Saturated.CoreUnfolder. -Require Import Crypto.Arithmetic.Saturated.WrappersUnfolder. -Require Import Crypto.Arithmetic.Saturated.Freeze. - -(** -<< -#!/bin/bash -for i in freeze freeze_cps; do - echo "Definition ${i}_sig := parameterize_sig (@Freeze.${i})."; - echo "Definition ${i} := parameterize_from_sig ${i}_sig."; - echo "Definition ${i}_eq := parameterize_eq ${i} ${i}_sig."; - echo "Hint Unfold ${i} : basesystem_partial_evaluation_unfolder."; - echo "Hint Rewrite <- ${i}_eq : pattern_runtime."; echo ""; -done ->> *) -Definition freeze_cps_sig := parameterize_sig (@Freeze.freeze_cps). -Definition freeze_cps := parameterize_from_sig freeze_cps_sig. -Definition freeze_cps_eq := parameterize_eq freeze_cps freeze_cps_sig. -Hint Unfold freeze_cps : basesystem_partial_evaluation_unfolder. -Hint Rewrite <- freeze_cps_eq : pattern_runtime. - -Definition freeze_sig := parameterize_sig (@Freeze.freeze). -Definition freeze := parameterize_from_sig freeze_sig. -Definition freeze_eq := parameterize_eq freeze freeze_sig. -Hint Unfold freeze : basesystem_partial_evaluation_unfolder. -Hint Rewrite <- freeze_eq : pattern_runtime. |