ocaml 3.09 transition

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

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 5d2dae3411eac2273133b7b5839805ee203a0662..33fb8fd78494085a819c9d65fb11e2020a654c42 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
@@ -123,9 +123,12 @@ let _ =
       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
     ]
 
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
-  ident ('/' ident)*                  (* path *)
+(*   ident ('/' ident)*                  |+ path +| *)
+  uri_step ('/' uri_step)*            (* path *)
   ('.' ident)+                        (* ext *)
   ("#xpointer(" number ('/' number)+ ")")?  (* xpointer *)