X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=3341b0febfea9fa55a2e96f0a889918dca41a8db;hb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a;hp=de300180ca994945dc42724de41c2e179ec86f6e;hpb=63f307e4cbec53919ce02d0ddcd7699a263a7f61;p=helm.git

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index de300180c..3341b0feb 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -189,8 +189,8 @@ let extract_term_production status pattern =
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
-        let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-        let action (env_opt : NotationEnv.t option) (loc : Ast.location) =
+        let _p_bindings, p_atoms, p_names, p_action = inner_pattern p in
+        let action (env_opt : NotationEnv.t option) (_loc : Ast.location) =
           match env_opt with
           | Some env -> List.map Env.opt_binding_some env
           | None -> List.map Env.opt_binding_of_name p_names
@@ -209,8 +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)
-          | 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),
@@ -357,11 +357,11 @@ let exc_located_wrapper f =
   try
     f ()
   with
-  | Stdpp.Exc_located (floc, Stream.Error msg) ->
+  | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
-  | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+  | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 
 let parse_level1_pattern grammars precedence lexbuf =
@@ -616,7 +616,8 @@ EXTEND
   ];
   arg: [
     [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN ->
+      typ = OPT [ SYMBOL ":"; typ = term -> typ] ; RPAREN -> (* FG: now type is optional *)
+        let ty = match typ with Some ty -> ty | None -> Ast.Implicit `JustOne in
         List.map (fun n -> Ast.Ident (n, None)) names, Some ty
     | name = IDENT -> [Ast.Ident (name, None)], None
     | blob = UNPARSED_META ->
@@ -657,7 +658,8 @@ EXTEND
         args = LIST1 arg;
         index_name = OPT [ "on"; id = single_arg -> id ];
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let rec position_of name p = function 
             | [] -> None, p
             | n :: _ when n = name -> Some p, p
@@ -695,7 +697,8 @@ EXTEND
         name = single_arg;
         args = LIST0 arg;
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let args =
            List.concat
             (List.map