diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-08-08 12:50:52 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-08 12:50:52 -0400 |
| commit | bc670dd9081811f55310bc3e2ea7432095fb3ef1 (patch) | |
| tree | 8d90fa801a5391ad58d21e45122b1e9b8e9125a8 /src/Spec | |
| parent | bd75013629d1572c411750b733707c8d4c45c21c (diff) | |
[cbv beta] in the beginning of Obligation Tactic for 8.5
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/ModularArithmetic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 80638ff58..95d7d4e75 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -22,7 +22,7 @@ Local Open Scope Z_scope. Module F. Definition F (m : BinInt.Z) := { z : BinInt.Z | z = z mod m }. - Local Obligation Tactic := auto using Pre.Z_mod_mod. + Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod. Program Definition of_Z m (a:BinNums.Z) : F m := a mod m. Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a. |