Remove the Sfacto constructor from Gramlib.

Used by rule factorisation in theory, but appears to be unused in Coq.

1 files changed, 0 insertions, 21 deletions

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 3b2c3de760..de9b1e864c 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -27,7 +27,6 @@ and 'te g_level =
     lprefix : 'te g_tree }
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
-    Sfacto of 'te g_symbol
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
@@ -65,7 +64,6 @@ let rec derive_eps =
     Slist0 _ -> true
   | Slist0sep (_, _, _) -> true
   | Sopt _ | Sflag _ -> true
-  | Sfacto s -> derive_eps s
   | Stree t -> tree_derive_eps t
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
@@ -90,21 +88,6 @@ let rec eq_symbol s1 s2 =
   | Sflag s1, Sflag s2 -> eq_symbol s1 s2
   | Sopt s1, Sopt s2 -> eq_symbol s1 s2
   | Stree _, Stree _ -> false
-  | Sfacto (Stree t1), Sfacto (Stree t2) ->
-      (* The only goal of the node 'Sfacto' is to allow tree comparison
-         (therefore factorization) without looking at the semantic
-         actions; allow factorization of rules like "SV foo" which are
-         actually expanded into a tree. *)
-      let rec eq_tree t1 t2 =
-        match t1, t2 with
-          Node n1, Node n2 ->
-            eq_symbol n1.node n2.node && eq_tree n1.son n2.son &&
-            eq_tree n1.brother n2.brother
-        | LocAct (_, _), LocAct (_, _) -> true
-        | DeadEnd, DeadEnd -> true
-        | _ -> false
-      in
-      eq_tree t1 t2
   | _ -> s1 = s2
 
 let is_before s1 s2 =
@@ -189,7 +172,6 @@ and token_exists_in_tree f =
   | LocAct (_, _) | DeadEnd -> false
 and token_exists_in_symbol f =
   function
-    Sfacto sy -> token_exists_in_symbol f sy
   | Slist0 sy -> token_exists_in_symbol f sy
   | Slist0sep (sy, sep, _) ->
       token_exists_in_symbol f sy || token_exists_in_symbol f sep
@@ -325,7 +307,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
           flush stderr;
           failwith "Grammar.extend error"
         end
-  | Sfacto s -> check_gram entry s
   | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist0 s -> check_gram entry s
@@ -353,7 +334,6 @@ let get_initial entry =
 let insert_tokens gram symbols =
   let rec insert =
     function
-      Sfacto s -> insert s
     | Slist0 s -> insert s
     | Slist1 s -> insert s
     | Slist0sep (s, t, _) -> insert s; insert t
@@ -487,7 +467,6 @@ let rec decr_keyw_use gram =
           Hashtbl.remove gram.gtokens tok;
           gram.glexer.Plexing.tok_removing tok
         end
-  | Sfacto s -> decr_keyw_use gram s
   | Slist0 s -> decr_keyw_use gram s
   | Slist1 s -> decr_keyw_use gram s
   | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2