From 6906417a548f47a888fa5a43470dc3c5d7e4442b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Oct 2012 10:59:51 +0000 Subject: [PATCH] One useless Obj.magic removed. --- matita/components/grafite_parser/grafiteParser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 024d321b4..4e5c709f7 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -50,7 +50,7 @@ let parsable_statement status buf = let parse_statement grafite_parser parsable = exc_located_wrapper - (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) (fst parsable))) + (fun () -> (Grammar.Entry.parse_parsable grafite_parser (fst parsable))) let strm_of_parsable (_,buf) = buf -- 2.39.2