aboutsummaryrefslogtreecommitdiffstats
path: root/src/Conversion_tactics.v
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2020-02-28 15:11:04 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2020-02-28 15:11:04 +0100
commiteaa6a62db567c61c9a40af816a9e839eefaffa21 (patch)
tree89c7cdd6bd65a4182a2a6448ebb4d469643f2e0a /src/Conversion_tactics.v
parentc296b2d06a70f1603916a2450ce49f6c98270a39 (diff)
downloadsmtcoq-eaa6a62db567c61c9a40af816a9e839eefaffa21.tar.gz
smtcoq-eaa6a62db567c61c9a40af816a9e839eefaffa21.zip
Remove useless code
Diffstat (limited to 'src/Conversion_tactics.v')
-rw-r--r--src/Conversion_tactics.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
index ecf1be8..cb0c090 100644
--- a/src/Conversion_tactics.v
+++ b/src/Conversion_tactics.v
@@ -457,4 +457,4 @@ End nat_convert_type.
Module nat_convert_mod := convert nat_convert_type.
-Ltac nat_convert := fold Nat.add Nat.mul Nat.leb Nat.ltb Nat.eqb; nat_convert_mod.convert.
+Ltac nat_convert := nat_convert_mod.convert.