]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParser0.ml
- added sanity checks entry
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser0.ml
index e89c00d22bff826ba72c507b2c01a9ef76f28187..fe4bf062346c95b9cf29eaeb692871f4fccab3fd 100644 (file)
@@ -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