From 82500d94be615e82fdb4564ff0daac2f5dcb156c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 12 Nov 2017 20:55:59 -0500 Subject: Split up reflective side condition tactics Now we no longer bundle the side-condition solver with the reifier --- src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/Compilers') diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 3e4f0fdbd..199d4e0b8 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -326,10 +326,8 @@ Ltac refine_with_pipeline_correct opts := The other choices are tactics that are specialized to the specific side-condition for which they are used (reification, boundedness of input, reduction of [Interp], renaming). *) -Ltac solve_side_conditions := +Ltac solve_post_reified_side_conditions := [> - (** ** reification *) - do_reify | (** ** pre-wf pipeline *) unify_abstract_vm_compute_rhs_reflexivity | (** ** reflective wf side-condition 1 *) @@ -360,7 +358,12 @@ Ltac solve_side_conditions := abstract handle_bounds_from_hyps | (** ** boundedness side-condition *) handle_boundedness_side_condition ]. - +Ltac solve_side_conditions := + [> + (** ** reification *) + do_reify | + .. ]; + solve_post_reified_side_conditions. (** ** The Entire Pipeline *) (** The [do_reflective_pipeline] tactic solves a goal of the form that -- cgit v1.2.3