X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParserContext.ml;h=c51346e1ac3940625b7866df6bb7f0d6a3a77e01;hb=71b08b1ea99893b3c5e2d91fc26e1ab7330fd33d;hp=ae21e5d2e0e8193bcd78da63708634e8609cf955;hpb=818c90057de4f3ca2e1971b267549fe146b89b6f;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index ae21e5d2e..c51346e1a 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
@@ -23,11 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~current_uri ~context lexer lexbuf =
+let main ~context ~metasenv lexer lexbuf ~register_aliases =
  (* Warning: higly non-reentrant code!!! *)
- CicTextualParser0.current_uri := current_uri ;
  CicTextualParser0.binders := context ;
- let res = CicTextualParser.main lexer lexbuf in
-  CicTextualParser0.binders := [] ;
-  res
+ 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
+      )
 ;;