From 2871663cadca8355764c64bc921b2fc6126efb2c Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Tue, 2 May 2017 14:49:13 +0100
Subject: Remove why3 from standard compiler

---
 docs/using-the-compiler.rst | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'docs')

diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst
index b74da213..890604b1 100644
--- a/docs/using-the-compiler.rst
+++ b/docs/using-the-compiler.rst
@@ -121,7 +121,6 @@ Input Description
         //   abi - ABI
         //   ast - AST of all source files (not supported atm)
         //   legacyAST - legacy AST of all source files
-        //   why3 - Why3 translated output
         //   devdoc - Developer documentation (natspec)
         //   userdoc - User documentation (natspec)
         //   metadata - Metadata
@@ -154,9 +153,9 @@ Input Description
           "*": {
             "*": [ "evm.sourceMap" ]
           },
-          // Enable the legacy AST and Why3 output of every single file.
+          // Enable the legacy AST output of every single file.
           "*": {
-            "": [ "legacyAST", "why3" ]
+            "": [ "legacyAST" ]
           }
         }
       }
@@ -180,7 +179,7 @@ Output Description
           ],
           // Mandatory: Error type, such as "TypeError", "InternalCompilerError", "Exception", etc
           type: "TypeError",
-          // Mandatory: Component where the error originated, such as "general", "why3", "ewasm", etc.
+          // Mandatory: Component where the error originated, such as "general", "ewasm", etc.
           component: "general",
           // Mandatory ("error" or "warning")
           severity: "error",
@@ -272,7 +271,5 @@ Output Description
             }
           }
         }
-      },
-      // Why3 output (string)
-      why3: ""
+      }
     }
-- 
cgit v1.2.3