Skip to content

Commit

Permalink
Silence a warning about name collision
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Nov 9, 2016
1 parent 22393a2 commit a1bbca9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ModularArithmetic/ModularBaseSystemOpt.v
Original file line number Diff line number Diff line change
Expand Up @@ -1071,7 +1071,7 @@ Section SquareRoots.
by (rewrite carry_mul_opt_correct by auto;
cbv [eq]; rewrite carry_mul_rep, mul_rep; reflexivity)
end.
let RHS := match goal with |- {vs | eq ?vs ?RHS} => RHS end in
let RHS := match goal with |- {vs | eq vs ?RHS} => RHS end in
let RHSf := match (eval pattern powx in RHS) with ?RHSf _ => RHSf end in
change ({vs | eq vs (Let_In powx RHSf)}).
match goal with
Expand Down

0 comments on commit a1bbca9

Please sign in to comment.