diff options
author | 2017-04-06 22:53:07 -0400 | |
---|---|---|
committer | 2017-04-06 22:53:07 -0400 | |
commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Compilers/Z/Bounds/Pipeline.v | |
parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) |
rename-everything
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline.v')
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v new file mode 100644 index 000000000..6c9cda840 --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -0,0 +1,20 @@ +(** * Reflective Pipeline *) +Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue. +Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics. +(** This file combines the various PHOAS modules in tactics, + culminating in a tactic [refine_reflectively], which solves a goal of the form +<< +cast_back_flat_const (?x args) = f (cast_back_flat_const args) + /\ Bounds.is_bounded_by ?bounds (?x args) +>> +while instantiating [?x] and [?bounds] with nicely-reduced constants. + *) + +Module Export Exports. + Export Glue.Exports. + Export ReflectiveTactics.Exports. +End Exports. + +Ltac refine_reflectively := + refine_to_reflective_glue; + do_reflective_pipeline. |