diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-02 12:21:44 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-03 15:08:18 -0400 |
| commit | a049f31b6d1cf26ce7fd34a7bafad5179e94c3b7 (patch) | |
| tree | 6d71670ed15f404daa2e28a58a10413de073d954 /src | |
| parent | 4227720f82bd43f8cb5905c092ee210dc6cf18a9 (diff) | |
Rename PreDefinitions to OutputType
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Definition.v | 2 | ||||
| -rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/OutputType.v (renamed from src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v) | 3 | ||||
| -rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/src/Reflection/Z/Bounds/Pipeline/Definition.v b/src/Reflection/Z/Bounds/Pipeline/Definition.v index 142e85833..a209213fe 100644 --- a/src/Reflection/Z/Bounds/Pipeline/Definition.v +++ b/src/Reflection/Z/Bounds/Pipeline/Definition.v @@ -1,7 +1,7 @@ (** * Reflective Pipeline: Main Pipeline Definition *) Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Z.Syntax. -Require Import Crypto.Reflection.Z.Bounds.Pipeline.PreDefinitions. +Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType. (** This file contains the definitions of the assembling of the various transformations that are used in the pipeline. There are two stages to the reflective pipeline, with different diff --git a/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v b/src/Reflection/Z/Bounds/Pipeline/OutputType.v index 8102fe2ee..301ee9e9c 100644 --- a/src/Reflection/Z/Bounds/Pipeline/PreDefinitions.v +++ b/src/Reflection/Z/Bounds/Pipeline/OutputType.v @@ -1,5 +1,4 @@ -(** * Definitions which are used in the pipeline, but shouldn't be changed *) -(** *** Definition of the output type of the post-Wf pipeline *) +(** * Definition of the output type of the post-Wf pipeline *) (** Do not change these definitions unless you're hacking on the entire reflective pipeline tactic automation. *) Require Import Crypto.Reflection.Syntax. diff --git a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v index 4d21458c2..d57c77504 100644 --- a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -9,7 +9,7 @@ Require Import Crypto.Reflection.Z.Bounds.Interpretation. Require Import Crypto.Reflection.Z.Bounds.Relax. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Z.Reify. -Require Import Crypto.Reflection.Z.Bounds.Pipeline.PreDefinitions. +Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType. Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SubstLet. |