diff --git a/docs/gtk-lang/alt-ergo.lang b/docs/gtk-lang/alt-ergo.lang
deleted file mode 100644
index 7103bd592..000000000
--- a/docs/gtk-lang/alt-ergo.lang
+++ /dev/null
@@ -1,228 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!--
-
- Author: Alain Mebsout
-
--->
-<language id="alt-ergo" _name="Alt-Ergo" version="2.0" _section="Sources">
-  <metadata>
-    <property name="mimetypes">text/x-alt-ergo</property>
-    <!-- Conflict with Why3 -->
-    <!-- <property name="globs">*.mlw;*.why</property> -->
-    <property name="block-comment-start">(*</property>
-    <property name="block-comment-end">*)</property>
-  </metadata>
-
-  <styles>
-    <style id="comment" _name="Comment" map-to="def:comment"/>
-    <!-- <style id="base-n-integer" _name="Base-N Integer"
-    map-to="def:base-n-integer"/> -->
-    <style id="real" _name="Real" map-to="def:floating-point"/>
-    <style id="integer" _name="Interger" map-to="def:decimal"/>
-    <style id="keyword" _name="Keyword" map-to="def:preprocessor"/>
-    <style id="toplevel" _name="Toplevel"  map-to="def:keyword"/>
-    <style id="operator" _name="Operator" map-to="def:preprocessor"/>
-    <style id="type" _name="Data Type" map-to="def:type"/>
-    <style id="label" _name="Labeled argument" map-to="def:type"/>
-    <style id="poly-variant" _name="Polymorphic Variant" map-to="def:type"/>
-    <style id="variant" _name="Variant Constructor" map-to="def:type"/>
-    <style id="type-var" _name="Type Variable" map-to="def:type"/>
-    <style id="boolean" _name="Boolean value" map-to="def:boolean"/>
-    <style id="error" _name="Error" map-to="def:error"/>
-    <style id="trigger" _name="Trigger" map-to="def:comment"/>
-    <style id="special" _name="Special" map-to="def:special-char"/>
-    <!-- <style id="axiom" _name="Axiom" map-to="def:function"/> -->
-    <style id="definition-name" _name="Name" map-to="def:function"/>
-    <style id="theory-name" _name="Theory" map-to="def:string"/>
-  </styles>
-
-  <definitions>
-    <define-regex id="digit">[0-9]</define-regex>
-    <define-regex id="hexa">[0-9a-fA-F]</define-regex>
-    <define-regex id="ident">[A-Za-z][A-Za-z0-9_']*</define-regex>
-    <define-regex id="exponent">[pP][-+]?[0-9][0-9]*</define-regex>
-    <!-- here's the main context -->
-    <context id="alt-ergo">
-      <include>
-
-	<context id="comment" style-ref="comment">
-	  <start>\(\*</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context ref="def:in-comment:*"/>
-	  </include>
-	</context>
-
-
-	<context id="boolean-constant" style-ref="boolean">
-	  <keyword>true</keyword>
-	  <keyword>false</keyword>
-	  <keyword>void</keyword>
-	</context>
-	<!-- Flow control & common keywords -->
-	<context id="keywords" style-ref="keyword">
-	  <keyword>and</keyword>
-	  <keyword>distinct</keyword>
-	  <keyword>else</keyword>
-	  <keyword>exists</keyword>
-	  <keyword>forall</keyword>
-	  <keyword>if</keyword>
-	  <keyword>in</keyword>
-	  <keyword>not</keyword>
-	  <keyword>or</keyword>
-	  <keyword>reach</keyword>
-	  <keyword>then</keyword>
-	  <keyword>with</keyword>
-	</context>
-	<context id="toplevel" style-ref="toplevel">
-	  <keyword>ac</keyword>
-	  <keyword>check</keyword>
-	  <keyword>cut</keyword>
-	  <keyword>include</keyword>
-	  <keyword>end</keyword>
-        </context>
-	<context id="types" style-ref="type">
-	  <!-- pervasives types -->
-	  <keyword>bool</keyword>
-	  <keyword>int</keyword>
-	  <keyword>bitv</keyword>
-	  <keyword>prop</keyword>
-	  <keyword>real</keyword>
-	  <keyword>unit</keyword>
-	  <!-- note: Some and None are highlighted as variants -->
-	</context>
-
-	<context id="special" style-ref="special">
-	  <match>\?</match>
-	</context>
-
-	<context id="integer" style-ref="integer">
-	  <match>-?\%{digit}(\%{digit})*</match>
-	</context>
-
-	<context id="real" style-ref="real">
-	  <match>-?\%{digit}(\%{digit})*\.(\%{digit})*</match>
-	</context>
-	<context id="hex-number" style-ref="real">
-	  <match>0x\%{hexa}(\%{hexa})*(\.(\%{hexa})*)?\%{exponent}</match>
-	</context>
-
-	<context id="poly-variant" style-ref="poly-variant">
-	  <match>`\%{ident}</match>
-	</context>
-
-	<context id="type-var" style-ref="type-var">
-	  <match>'\%{ident}</match>
-	</context>
-
-	<!-- <context id="ident"> -->
-	<!--   <match>\%{ident}</match> -->
-	<!-- </context> -->
-
-	<context id="bitv" style-ref="integer">
-	  <match>\[[01][01]*\]</match>
-	</context>
-
-	<context id="op" style-ref="operator">
-	  <match>\|-&gt;|&lt;-&gt;|-&gt;|[\%\*+-]</match>
-	</context>
-
-        <context id="type" style-ref="toplevel">
-          <match>type\s+((('\%{ident}|\('\%{ident}(, '\%{ident})*\)) )?\%{ident})</match>
-          <include>
-            <context id="type-name" sub-pattern="1"
-                     style-ref="type"/>
-          </include>
-        </context>
-
-        <context id="logic">
-          <match>(logic)\s+(\%{ident})(\s*,\s*(\%{ident}))*</match>
-          <include>
-            <context id="logic-name" sub-pattern="1"
-                     style-ref="toplevel"/>
-            <context id="logic-name" sub-pattern="2"
-                     style-ref="definition-name"/>
-            <context id="logic-name" sub-pattern="4"
-                     style-ref="definition-name"/>
-          </include>
-        </context>
-
-        <context id="axiom" style-ref="toplevel">
-          <match>axiom\s+(\%{ident})</match>
-          <include>
-            <context id="axiom-name" sub-pattern="1"
-                     style-ref="definition-name"/>
-          </include>
-        </context>
-
-        <context id="hypothesis" style-ref="toplevel">
-          <match>hypothesis\s+(\@?_?\%{ident})</match>
-          <include>
-            <context id="hyp-name" sub-pattern="1"
-                     style-ref="definition-name"/>
-          </include>
-        </context>
-
-        <context id="goal" style-ref="toplevel">
-          <match>goal\s+(\%{ident})</match>
-          <include>
-            <context id="goal-name" sub-pattern="1"
-                     style-ref="definition-name"/>
-          </include>
-        </context>
-
-        <context id="theory_ext" style-ref="toplevel">
-          <match>theory\s+(\%{ident})\s+extends\s+(\%{ident})</match>
-          <include>
-            <context id="theory-name" sub-pattern="1"
-                     style-ref="theory-name"/>
-            <context id="theoey-extend-name" sub-pattern="2"
-                     style-ref="theory-name"/>
-          </include>
-        </context>
-
-        <context id="theory" style-ref="toplevel">
-          <match>theory\s+(\%{ident})</match>
-          <include>
-            <context id="theory-name" sub-pattern="1"
-                     style-ref="theory-name"/>
-          </include>
-        </context>
-
-        <context id="function" style-ref="toplevel">
-          <match>(function|predicate|inversion|rewriting|instance)\s+(\%{ident})</match>
-          <include>
-            <context id="function-k" sub-pattern="1"
-                     style-ref="toplevel"/>
-            <context id="function-name" sub-pattern="2"
-                     style-ref="definition-name"/>
-          </include>
-        </context>
-
-	<context id="trigger" style-ref="trigger">
-	  <!-- <match>\[.*\]({.*})?(\s|\n)*\.</match> -->
-	  <start> \[</start>
-	  <end>(\]|})\.</end>
-	  <include>
-	    <context ref="boolean-constant"/>
-	    <context ref="keywords"/>
-	    <context ref="types"/>
-	    <context ref="special"/>
-	    <context ref="integer"/>
-	    <context ref="real"/>
-	    <context ref="hex-number"/>
-	    <context ref="poly-variant"/>
-	    <context ref="op"/>
-	    <context ref="type-var"/>
-	    <context ref="bitv"/>
-	  </include>
-	</context>
-<!--
-	<context id="badtrigger" style-ref="error" extend-parent="false">
-	  <match>\]</match>
-	</context>
--->
-      </include>
-    </context>
-  </definitions>
-</language>