X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=32b6b0a9068312564dcc8c65648b12892a6f4bc3;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bcfd6c9f62282e15163a5e988beb3a736702d41a;hpb=71adb7c2f7f84e6bfe523cf066a65cc14cc9217b;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index bcfd6c9f6..32b6b0a90 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -46,8 +46,6 @@ let term = Grammar.Entry.create level2_ast_grammar "term"
 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
-let return_term loc term = ()
-
 let int_of_string s =
   try
     Pervasives.int_of_string s
@@ -425,7 +423,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];
@@ -588,9 +586,9 @@ EXTEND
       | m = META; s = meta_substs ->
           return_term loc (Ast.Meta (int_of_string m, s))
       | s = sort -> return_term loc (Ast.Sort s)
-      | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
-        "match"; t = term;
+      | "match"; t = term;
         indty_ident = OPT [ "in"; id = IDENT -> id, None ];
+        outtyp = OPT [ "return"; ty = term -> ty ];
         "with"; SYMBOL "[";
         patterns = LIST0 [
           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);