More granularity in src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v

1 files changed, 12 insertions, 4 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 199d4e0b8..0b9d364dd 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -290,17 +290,25 @@ End with_round_up_list.
     [PipelineCorrect] lemma to create side-conditions.  It assumes the
     goal is in exactly the form given in the conclusion of the
     [PipelineCorrect] lemma. *)
-
+(** The [refine_PipelineSideConditions_constructor] subtactic splits
+    up the [PipelineSideConditions] record goal into multiple
+    subgoals, to be discharged by automation lower in this file
+    ([solve_post_reified_side_conditions]). *)
+Ltac refine_PipelineSideConditions_constructor :=
+  lazymatch goal with
+  | [ |- PipelineSideConditions ?opts ?evars _ ]
+    => simple refine {| Hevar := _ |};
+       cbv [b e' e_final e_final_newtype e e_pre_pkg e_pkg proj1_sig]
+  end.
 Ltac refine_with_pipeline_correct opts :=
   lazymatch goal with
   | [ |- _ /\ ?castback ?fW = ?fZ ?arg ]
     => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ {| e_pkg := _ |}) in
-       simple refine (lem _ {| Hevar := _ |});
-       cbv beta iota delta [b e' e_final e_final_newtype e e_pre_pkg e_pkg];
+       simple refine (lem _ _);
        subst fW fZ
   end;
   [ eexists
-  | cbv [proj1_sig].. ].
+  | refine_PipelineSideConditions_constructor ].
 
 (** The tactic [solve_side_conditions] uses the above
     reduction-and-proving-equality tactics to prove the