From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 21 Oct 2011 15:35:14 +0000 (+0000)
Subject: Now it should compile :-)
X-Git-Tag: make_still_working~2160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=988cf01c5bd740d6e75767327f201a3c43d635ed;p=helm.git

Now it should compile :-)
---

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 720b4196a..9e1e54ee7 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -538,7 +538,7 @@ EXTEND
   grafite_ncommand: [ [
       IDENT "qed" ;  b = OPT SYMBOL "-" -> 
       let b = match b with None -> true | Some _ -> false in
-      if not b then G.NQed (loc,b)
+      G.NQed (loc,b)
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml
index 738ceb4da..5bc87f247 100644
--- a/matita/components/grafite_parser/print_grammar.ml
+++ b/matita/components/grafite_parser/print_grammar.ml
@@ -87,7 +87,7 @@ and is_symbol_dummy = function
   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
   | Snterm e | Snterml (e, _) -> is_entry_dummy e
   | Slist1 x | Slist0 x -> is_symbol_dummy x
-  | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
+  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
   | Sopt x -> is_symbol_dummy x
   | Sself | Snext -> false
   | Stree t -> is_tree_dummy t
@@ -186,7 +186,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]} @ ";
         todo
-    | Slist0sep (symbol,sep,false) ->
+    | Slist0sep (symbol,sep) ->
         Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "{@[<hov2> ";
@@ -200,7 +200,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]}+ @ ";
         todo 
-    | Slist1sep (symbol,sep,false) ->
+    | Slist1sep (symbol,sep) ->
         let todo = visit_symbol symbol todo is_son  in
         Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol sep todo is_son in