Syntactic change:

 [ ... ] match t in t with ==> match t in t return ... with

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 5d2dae3411eac2273133b7b5839805ee203a0662..3d9d6be252a3d28118d1d1f5e7af47630928d4e1 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -107,7 +107,7 @@ let level2_ast_keywords = Hashtbl.create 23
 let _ =
   List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match";
-    "with"; "in"; "and"; "to"; "as"; "on" ]
+    "with"; "in"; "and"; "to"; "as"; "on"; "return" ]
 
 let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k ()
 let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k

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>> (* ⇒ *);

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index aa171c55ccedd2aed0a86da4b99de8b0e73b08b8..27040d5ae8d41138bb098001bb395ea377eb487a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -158,19 +158,25 @@ let pp_ast0 t k =
           match outty_opt with
           | None -> []
           | Some outty ->
-              [ builtin_symbol "["; remove_level_info (k outty);
-                builtin_symbol "]"; break ]
+              [ keyword "return"; break; remove_level_info (k outty)]
         in
         let indty_box =
           match indty_opt with
           | None -> []
-          | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ]
+          | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ]
         in
         let match_box =
-          hvbox false true [
-            keyword "match"; break;
-            hvbox false false ([ top_pos (k what) ] @ indty_box); break;
-            keyword "with" ]
+          hvbox false false [
+           hvbox false true [
+            hvbox false true [ keyword "match"; break; top_pos (k what) ];
+            break;
+            hvbox false true indty_box;
+            break;
+            hvbox false true outty_box
+           ];
+           break;
+           keyword "with"
+         ]
         in
         let mk_case_pattern (head, href, vars) =
           hbox true false (ident_w_href href head :: List.map aux_var vars)
@@ -209,7 +215,7 @@ let pp_ast0 t k =
         in
         add_level_info Ast.simple_prec Ast.simple_assoc
           (hvbox false false [
-            hvbox false false (outty_box @ [ match_box ]); break;
+            hvbox false false ([match_box]); break;
             hbox false false [ hvbox false false patterns'' ] ])
     | Ast.Cast (bo, ty) ->
         add_level_info Ast.simple_prec Ast.simple_assoc