From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 12 Dec 2011 15:37:04 +0000 (+0000)
Subject: Re-Ported to
X-Git-Tag: make_still_working~2029
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9861eb06735d8a60c41687efea26ccd81c67b9c8;p=helm.git

Re-Ported to

- camlp5 version 6.02.2 + patches
- ocaml version 3.11.2-4

If you are still using the old version of OCaml + Camlp5, do not update
these two files.
---

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 00ac411fa..a9307012f 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -209,10 +209,8 @@ let extract_term_production status pattern =
           match magic with
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
-(*          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)*)
-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),