Coq: ignore the "type unit = ()" declaration in why3.Unit

4f841f92 · Andrei Paskevich · 5e4507b3 · 4f841f92 · 4f841f92
Commit 4f841f92 authored May 20, 2017 by Andrei Paskevich
Hide whitespace changes
Inline Side-by-side

Showing with 9 additions and 0 deletions

drivers/coq-common.gen drivers/coq-common.gen +5 -0

drivers/coq-ssreflect.drv drivers/coq-ssreflect.drv +4 -0

No files found.
--- a/drivers/coq-common.gen
+++ b/drivers/coq-common.gen
@@ -24,6 +24,11 @@ theory BuiltIn
  syntax predicate  (=)   "(%1 = %2)"
 end

+
+theory Unit
+  syntax type unit "unit"
+end
+
 theory Bool

  syntax type bool   "bool"

--- a/drivers/coq-ssreflect.drv
+++ b/drivers/coq-ssreflect.drv
@@ -34,6 +34,10 @@ Unset Printing Implicit Defensive.

 end

+theory Unit
+  syntax type unit "unit"
+end
+
 theory HighOrd
  syntax type (->) "(%1 -> %2)"
  syntax function (@)  "(%1 %2)"