diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-10 18:53:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-10 18:53:06 -0400 |
| commit | 0f7aa8286bea48d1a779e9837303da1df8572488 (patch) | |
| tree | de56add3b1339785df0bb2723d06a58ae8680bf6 /src/Compilers/Named/MapCastInterp.v | |
| parent | eaf7fba1612c8ba2987b40bafc6b4e20a5f0be0b (diff) | |
Reorder parameters for ease of partial instantiation, add symbolic_expr_dec
Diffstat (limited to 'src/Compilers/Named/MapCastInterp.v')
| -rw-r--r-- | src/Compilers/Named/MapCastInterp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v index cb4d3062c..ad067af64 100644 --- a/src/Compilers/Named/MapCastInterp.v +++ b/src/Compilers/Named/MapCastInterp.v @@ -95,11 +95,11 @@ Section language. | _ => handle_options_step (* preprocess *) | [ H : context[lookupb (extend _ _ _) _] |- _ ] - => first [ rewrite (fun C => lookupb_extend C base_type_dec Name_dec) in H by assumption - | setoid_rewrite (fun C => lookupb_extend C base_type_dec Name_dec) in H; [ | assumption.. ] ] + => first [ rewrite (lookupb_extend base_type_dec Name_dec) in H by assumption + | setoid_rewrite (lookupb_extend base_type_dec Name_dec) in H; [ | assumption.. ] ] | [ |- context[lookupb (extend _ _ _) _] ] => first [ rewrite (fun C => lookupb_extend C base_type_dec Name_dec) by assumption - | setoid_rewrite (fun C => lookupb_extend C base_type_dec Name_dec); [ | assumption.. ] ] + | setoid_rewrite (lookupb_extend base_type_dec Name_dec); [ | assumption.. ] ] | _ => progress subst (* handle multiple hypotheses *) | [ H : find_Name _ ?n ?N = Some ?t', H'' : context[find_Name_and_val _ _ ?t ?n ?N ?x ?default] |- _ ] |