diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-02 23:56:47 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-03 15:08:18 -0400 |
| commit | 99282c8e7b1bd6339af107c7c96a0f588ae8c2ff (patch) | |
| tree | d0ace44cc4ffb98f4dc3dafd09622fb3d16fbe54 /src | |
| parent | 6d4d8bbacefa9bdc957e28de37a777d21ab978ec (diff) | |
Fix missing unfold in proof
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Definition.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/Z/Bounds/Pipeline/Definition.v b/src/Reflection/Z/Bounds/Pipeline/Definition.v index 2e0e24d43..1c2508bd7 100644 --- a/src/Reflection/Z/Bounds/Pipeline/Definition.v +++ b/src/Reflection/Z/Bounds/Pipeline/Definition.v @@ -62,6 +62,7 @@ Require Import Crypto.Reflection.LinearizeWf. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijn. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnInterp. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnWf. +Require Import Crypto.Util.Sigma. (** *** Definition of the Post-Wf Pipeline *) (** Do not change the name or the type of this definition *) @@ -112,7 +113,7 @@ Definition PostWfPipelineCorrect /\ cast_back_flat_const (Interp interp_op e' v') = Interp interp_op e v. Proof. (** These first two lines probably shouldn't change much *) - unfold PostWfPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map in *. + unfold PostWfPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *. repeat (break_match_hyps || inversion_option || inversion_ProcessedReflectivePackage || inversion_sigma || eliminate_hprop_eq || inversion_prod || simpl in * || subst). |