ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 578a9d6f04ae7d116dbd88f2773d51427c1ab1ff..32b6b0a9068312564dcc8c65648b12892a6f4bc3 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -586,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>> (* ⇒ *);