diff options
Diffstat (limited to 'plugins/rtauto/Bintree.v')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 600e8993b4..99c02995fb 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -319,6 +319,9 @@ Arguments F_empty [A]. Arguments F_push [A] a S _. Arguments In [A] x S F. +Register empty as plugins.rtauto.empty. +Register push as plugins.rtauto.push. + Section Map. Variables A B:Set. |