]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
* if no configuration file is found, issue a warning but doesn't crash
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.ml
index c51346e1ac3940625b7866df6bb7f0d6a3a77e01..6901bd48c28317c262a5444590e31f60cffdf83a 100644 (file)
  * 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
 ;;