diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-20 13:42:00 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | a3e42efc86e20c8db07cb0c013b56ed25fb28334 (patch) | |
| tree | b3dfa1b80282a6ed2a82b08a2594c0cddcfc15b6 | |
| parent | af5141847d7888e502e90b56646959fbf1070b76 (diff) | |
src/Tactics/Algebra_syntax/Nsatz.v: power 1 only
| -rw-r--r-- | src/Tactics/Algebra_syntax/Nsatz.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v index b59f68120..e219bc579 100644 --- a/src/Tactics/Algebra_syntax/Nsatz.v +++ b/src/Tactics/Algebra_syntax/Nsatz.v @@ -125,7 +125,7 @@ Ltac nsatz_power power := let power_N := (eval compute in (BinNat.N.of_nat power)) in nsatz_sugar_power BinInt.Z0 power_N. -Ltac nsatz := nsatz_power 1%nat || nsatz_power 2%nat || nsatz_power 3%nat || nsatz_power 4%nat || nsatz_power 5%nat. +Ltac nsatz := nsatz_power 1%nat. Tactic Notation "nsatz" := nsatz. Tactic Notation "nsatz" constr(n) := nsatz_power n. |