diff --git a/tests/eunify.v b/tests/eunify.v index c12cc61862ee34ff378f3f5f5142eb61d0210f32..96eb3e66b2ce3a9d55504762cb18dd8b5d60f7bd 100644 --- a/tests/eunify.v +++ b/tests/eunify.v @@ -1,4 +1,5 @@ From stdpp Require Import tactics strings. +Unset Mangle Names. Check "eunify_test". Lemma eunify_test : ∀ x y, 0 < S x + y.