diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-12 20:55:59 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-13 00:26:41 -0500 |
| commit | 82500d94be615e82fdb4564ff0daac2f5dcb156c (patch) | |
| tree | f5fcdabfbef909de92ebedcb7ccc79a0815b08f2 /src/Compilers | |
| parent | 885b450606ee5fc4ae43e0411f1b929f193fb6b6 (diff) | |
Split up reflective side condition tactics
Now we no longer bundle the side-condition solver with the reifier
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 11 |
1 files changed, 7 insertions, 4 deletions
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 |