* http://cs.unibo.it/helm/.
*)
-let main ~context ~metasenv lexer lexbuf ~register_aliases =
+let main ~context ~metasenv lexer lexbuf =
(* Warning: higly non-reentrant code!!! *)
CicTextualParser0.binders := context ;
CicTextualParser0.metasenv := metasenv ;
- match CicTextualParser.main lexer lexbuf register_aliases with
- None -> None
- | Some (dom,mk_term) ->
- Some
- (dom,
- function interp ->
- let term = mk_term interp in
- let metasenv = !CicTextualParser0.metasenv in
- metasenv,term
- )
+ let dom,mk_term = CicTextualParser.main lexer lexbuf in
+ dom,
+ function interp ->
+ let term = mk_term interp in
+ let metasenv = !CicTextualParser0.metasenv in
+ metasenv,term
;;