X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.expanded.ml;h=5c73d2b4c4dec01a6808075289214cd6357d9834;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=fcbc081a7474d9e8b4f61bf95ff92cfc906c32cd;hpb=9230a8085102cd39258c047949e87001be6ffcf0;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
index fcbc081a7..5c73d2b4c 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
@@ -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 =
@@ -106,7 +96,9 @@ let extract_term_production pattern =
     | Layout l -> aux_layout l
     | Magic m -> aux_magic m
     | Variable v -> aux_variable v
-    | t -> prerr_endline (CicNotationPp.pp_term t); assert false
+    | t ->
+        prerr_endline (CicNotationPp.pp_term t);
+        assert false
   and aux_literal =
     function
       `Symbol s -> [NoBinding, symbol s]
@@ -125,7 +117,7 @@ let extract_term_production pattern =
         [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @
           aux p1
     | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
+(*     | Break -> [] *)
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
@@ -144,7 +136,6 @@ let extract_term_production pattern =
         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
         let env0 = List.map list_binding_of_name p_names in
         let grow_env_entry env n v =
-          prerr_endline "grow_env_entry";
           List.map
             (function
                n', (ty, ListValue vl) as entry ->
@@ -153,12 +144,11 @@ let extract_term_production pattern =
             env
         in
         let grow_env env_i env =
-          prerr_endline "grow_env";
           List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env
             env_i
         in
         let action (env_list : env_type list) (loc : location) =
-          prerr_endline "list action"; List.fold_right grow_env env_list env0
+          List.fold_right grow_env env_list env0
         in
         let g_symbol s =
           match magic with
@@ -183,14 +173,9 @@ let extract_term_production pattern =
   and inner_pattern p =
     let (p_bindings, p_atoms) = List.split (aux p) in
     let p_names = flatten_opt p_bindings in
-    let _ =
-      prerr_endline
-        ("inner names: " ^ String.concat " " (List.map fst p_names))
-    in
     let action =
       make_action
-        (fun (env : env_type) (loc : location) ->
-           prerr_endline "inner action"; env)
+        (fun (env : env_type) (loc : location) -> env)
         p_bindings
     in
     p_bindings, p_atoms, p_names, action
@@ -212,7 +197,6 @@ let extend level1_pattern ?(precedence = default_precedence) =
     let level = level_of_int precedence in
     let p_names = flatten_opt p_bindings in
     let _ =
-      prerr_endline (string_of_int (List.length p_bindings));
       Grammar.extend
         [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e),
          Some (Gramext.Level level),
@@ -975,8 +959,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) ->