merged cic_notation with disambiguation: good luck!

[helm.git] / helm / ocaml / cic_disambiguation / disambiguateTypes.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index 64fcdb5a839cc279a9575e52aea72c68bfcdb9b2..c30316769b5cb1ad94dce5a26bc899c197120d8f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -23,16 +23,20 @@
  * http://helm.cs.unibo.it/
  *)
 
-type term = CicAst.term
-type tactic = (term, string) TacticAst.tactic
-type tactical = (term, string) TacticAst.tactical
-type script_entry = Command of tactical | Comment of CicAst.location * string
-type script = CicAst.location * script_entry list
+type term = CicNotationPt.term
+type tactic = (term, string) GrafiteAst.tactic
+type tactical = (term, string) GrafiteAst.tactical
+type script_entry =
+  | Command of tactical
+  | Comment of CicNotationPt.location * string
+type script = CicNotationPt.location * script_entry list
 
 type domain_item =
- | Id of string               (* literal *)
- | Symbol of string * int     (* literal, instance num *)
- | Num of int                 (* instance num *)
+  | Id of string               (* literal *)
+  | Symbol of string * int     (* literal, instance num *)
+  | Num of int                 (* instance num *)
+
+exception Invalid_choice
 
 module OrderedDomain =
   struct