]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.expanded.ml
changed default parameter values...
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.expanded.ml
index 7b90be54a144ab610d6e2297c73c05a9b93000e2..5c73d2b4c4dec01a6808075289214cd6357d9834 100644 (file)
@@ -96,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]
@@ -115,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
@@ -134,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 ->
@@ -143,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
@@ -173,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
@@ -202,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),