From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [coqlib] Rebindable Coqlib namespace. We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- test-suite/success/btauto.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/success/btauto.v (limited to 'test-suite') diff --git a/test-suite/success/btauto.v b/test-suite/success/btauto.v new file mode 100644 index 0000000000..d2512b5cbb --- /dev/null +++ b/test-suite/success/btauto.v @@ -0,0 +1,9 @@ +Require Import Btauto. + +Open Scope bool_scope. + +Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true. +Proof. btauto. Qed. + +Lemma test_xorb a : xorb a a = false. +Proof. btauto. Qed. -- cgit v1.2.3