X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParserContext.ml;h=e14259589c2ea4bc330815e150d8fd42eaeb7d78;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=28581bc5875f5e1f5aff9f4a6394eea090601ed6;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml index 28581bc58..e14259589 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml @@ -28,9 +28,11 @@ let main ~context ~metasenv lexer lexbuf = TexCicTextualParser0.binders := context ; TexCicTextualParser0.metasenv := metasenv ; let dom,mk_term = TexCicTextualParser.main lexer lexbuf in - dom, - function interp -> - let term = mk_term interp in - let metasenv = !TexCicTextualParser0.metasenv in - metasenv,term + let metasenv' = !TexCicTextualParser0.metasenv in + dom, + function interp -> + TexCicTextualParser0.metasenv := metasenv' ; + let term = mk_term interp in + let metasenv = !TexCicTextualParser0.metasenv in + metasenv,term ;;