X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser0.ml;h=fe4bf062346c95b9cf29eaeb692871f4fccab3fd;hb=5a369548a2f04fb59b5cbb94526325aae9bf415a;hp=e89c00d22bff826ba72c507b2c01a9ef76f28187;hpb=818c90057de4f3ca2e1971b267549fe146b89b6f;p=helm.git diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml index e89c00d22..fe4bf0623 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml @@ -26,4 +26,9 @@ exception Eof;; let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");; -let binders = ref ([] : Cic.name list);; +let binders = ref ([] : (Cic.name option) list);; +let metasenv = ref ([] : Cic.metasenv);; +let locate_object = ref ((fun _ -> None):string->Cic.term option);; + +let set_locate_object f = + locate_object := f