]> matita.cs.unibo.it Git - helm.git/commitdiff
removed a line of dead code
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 23 Sep 2005 13:46:46 +0000 (13:46 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 23 Sep 2005 13:46:46 +0000 (13:46 +0000)
helm/ocaml/cic_notation/cicNotationParser.ml

index 4622f67a6f1eff41881d7c3939a3dfe55fc9097d..578a9d6f04ae7d116dbd88f2773d51427c1ab1ff 100644 (file)
@@ -46,8 +46,6 @@ let term = Grammar.Entry.create level2_ast_grammar "term"
 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 
-let return_term loc term = ()
-
 let int_of_string s =
   try
     Pervasives.int_of_string s