Added module DiscriminationTactics with brand new tactics Injection and

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser0.ml

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index fe4bf062346c95b9cf29eaeb692871f4fccab3fd..fab36396087cb41a1ab691e71a9c28f4d4d3a6fd 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -25,10 +25,17 @@
 
 exception Eof;;
 
-let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
+type uri =
+   ConUri of UriManager.uri
+ | VarUri of UriManager.uri
+ | IndTyUri of UriManager.uri * int
+ | IndConUri of UriManager.uri * int * int
+;;
+
+type interp_codomain =
+   Uri of uri
+ | Implicit
+;;
+
 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