]> 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 0adf84723ce7587f88c66f5018a3d8320e373f68..5d103bdaafedd1fca028efd1f570f4af5bb9d375 100644 (file)
@@ -134,7 +134,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 ->
@@ -143,12 +142,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
@@ -173,14 +171,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
@@ -202,7 +195,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),