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 /src/Tactics/Algebra_syntax | |
parent | af5141847d7888e502e90b56646959fbf1070b76 (diff) |
src/Tactics/Algebra_syntax/Nsatz.v: power 1 only
Diffstat (limited to 'src/Tactics/Algebra_syntax')
-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. |