diff options
Diffstat (limited to 'plugins/nsatz/NsatzR.v')
| -rw-r--r-- | plugins/nsatz/NsatzR.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v index d8d1a91b4..2009dc16d 100644 --- a/plugins/nsatz/NsatzR.v +++ b/plugins/nsatz/NsatzR.v @@ -396,7 +396,6 @@ Ltac nsatzR := nsatzRpv 6%N 1%Z (@nil R) (@nil R). Ltac nsatzRradical radicalmax := nsatzRpv radicalmax 1%Z (@nil R) (@nil R). Ltac nsatzRparameters lparam := nsatzRpv 6%N 1%Z lparam (@nil R). -Tactic Notation "nsatz" := nsatzR. Tactic Notation "nsatz" "with" "lexico" := nsatzRpv 6%N 2%Z (@nil R) (@nil R). Tactic Notation "nsatz" "with" "lexico" "sugar":= |