]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.expanded.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.expanded.ml
index fcbc081a7474d9e8b4f61bf95ff92cfc906c32cd..7b90be54a144ab610d6e2297c73c05a9b93000e2 100644 (file)
@@ -54,37 +54,27 @@ ttype binding =
 llet make_action action bindings =
   let rec aux (vl : env_type) =
     function
-      [] ->
-        prerr_endline "aux: make_action";
-        Gramext.action (fun (loc : location) -> action vl loc)
-    | NoBinding :: tl ->
-        prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl)
+      [] -> Gramext.action (fun (loc : location) -> action vl loc)
+    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
     | Binding (name, TermType) :: tl ->
-        prerr_endline "aux: term";
         Gramext.action
           (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
     | Binding (name, StringType) :: tl ->
-        prerr_endline "aux: string";
         Gramext.action
           (fun (v : string) ->
              aux ((name, (StringType, StringValue v)) :: vl) tl)
     | Binding (name, NumType) :: tl ->
-        prerr_endline "aux: num";
         Gramext.action
           (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
     | Binding (name, OptType t) :: tl ->
-        prerr_endline "aux: opt";
         Gramext.action
           (fun (v : 'a option) ->
              aux ((name, (OptType t, OptValue v)) :: vl) tl)
     | Binding (name, ListType t) :: tl ->
-        prerr_endline "aux: list";
         Gramext.action
           (fun (v : 'a list) ->
              aux ((name, (ListType t, ListValue v)) :: vl) tl)
-    | Env _ :: tl ->
-        prerr_endline "aux: env";
-        Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
+    | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
   in
   aux [] (List.rev bindings)
 llet flatten_opt =
@@ -975,8 +965,7 @@ let _ =
         [Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
-             (prerr_endline "number"; return_term loc (Num (n, 0)) :
-              'l2_pattern));
+             (return_term loc (Num (n, 0)) : 'l2_pattern));
         [Gramext.Stoken ("URI", "")],
         Gramext.action
           (fun (u : string) (loc : Lexing.position * Lexing.position) ->