X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=1e6860281c0fcee7eb433b6c62108aca0b854ad3;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=38ce016768914215913ebb4ae0c2c047a6ece4a5;hpb=da71c09b8f4a42d3273fcbaea0cda3bceed1d949;p=helm.git

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 38ce01676..1e6860281 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -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 =
@@ -657,7 +657,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 +696,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