From ae71be249b6d0e3fcf4d5d14bd2282dd63cb4a4c Mon Sep 17 00:00:00 2001
From: Gabriel Kerneis
Date: Wed, 23 Oct 2013 17:16:08 +0100
Subject: Don't export list of types to ML AST

---
 language/l2.lem | 4 ----
 language/l2.ml  | 5 -----
 language/l2.ott | 2 +-
 3 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/language/l2.lem b/language/l2.lem
index 90974dfc..d39c7110 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -283,10 +283,6 @@ type def =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
-type ts = 
- | Ts_lst of list t
-
-
 type defs =  (* Definition sequence *)
  | Defs of list def
 
diff --git a/language/l2.ml b/language/l2.ml
index feb1ca32..bf87b48b 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -456,11 +456,6 @@ type
  | Typ_lib_reg of typ (* mutable register components holding typ *)
 
 
-type 
-ts = 
-   Ts_lst of (t) list
-
-
 type 
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
diff --git a/language/l2.ott b/language/l2.ott
index f129d9c4..2e37a490 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1215,7 +1215,7 @@ terminals :: '' ::=
   | consistent_decrease                 :: :: cd
     {{ tex \ottkw{consistent\_decrease}~ }}
 
-ts :: ts_ ::=
+ts :: ts_ ::=                                     {{ phantom }}
   | t1 , .. , tn :: :: lst 
 
 formula :: formula_ ::=
-- 
cgit v1.2.3