Skip to content

Commit

Permalink
Fix a build issue
Browse files Browse the repository at this point in the history
When Rewriter/Reify is required before the abs int proofs, the code
fails without this due to `Global Arguments` settings.
  • Loading branch information
JasonGross committed Oct 15, 2019
1 parent 0a90e79 commit 0c63685
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/AbstractInterpretation/Wf.v
Original file line number Diff line number Diff line change
Expand Up @@ -796,6 +796,8 @@ Module Compilers.
(expr.Ident ident.Z_cast2)
(#(@ident.Literal base.type.zrange r1%zrange), #(@ident.Literal base.type.zrange r2%zrange))%expr_pat).

Local Arguments base.try_make_transport_cps / _ _ _.
Local Arguments type.try_make_transport_cps / _ _ _ _ _.
Lemma is_annotated_for_spec {relax_zrange var} t t' e st
: @is_annotated_for relax_zrange var t t' e st = true
<-> ((exists (pf : t' = tZ) r,
Expand Down

0 comments on commit 0c63685

Please sign in to comment.