X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.expanded.ml;h=0adf84723ce7587f88c66f5018a3d8320e373f68;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;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..0adf84723 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 = @@ -125,7 +115,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 @@ -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) ->