Skip to content

GitLab

Commit bd28ab82 authored by Michael Sammler's avatar Michael Sammler
Browse files

Revert "never simpl bool_decide" 

This reverts commit bcf29bb3.
parent bcf29bb3
Pipeline #55227 passed with stage
in 13 minutes and 55 seconds
Show whitespace changes
Inline Side-by-side
theories/lithium/base.v
View file @ bd28ab82
...@@ -23,7 +23,6 @@ Typeclasses Opaque is_Some. ...@@ -23,7 +23,6 @@ Typeclasses Opaque is_Some.
Global Opaque rotate_nat_add rotate_nat_sub. Global Opaque rotate_nat_add rotate_nat_sub.
Typeclasses Opaque Z.divide Z.modulo Z.div Z.shiftl Z.shiftr. Typeclasses Opaque Z.divide Z.modulo Z.div Z.shiftl Z.shiftr.
Arguments bool_decide : simpl never.
Arguments min : simpl nomatch. Arguments min : simpl nomatch.
Arguments Z.testbit : simpl never. Arguments Z.testbit : simpl never.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment