merged cic_notation with disambiguation: good luck!

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index ca33fa4226db2cdd4c667b1090692eb43634faa6..6f74c23c0ab674bcf213a60992e4544c0574ff55 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -29,9 +29,9 @@ exception NoWellTypedInterpretation
 exception PathNotWellFormed
 
 val interpretate_path :
- context:Cic.name list -> env:DisambiguateTypes.environment -> CicAst.term ->
-  Cic.term
-
+  context:Cic.name list -> env:DisambiguateTypes.environment ->
+  DisambiguateTypes.term ->
+    Cic.term
 
 module type Disambiguator =
 sig
@@ -41,7 +41,7 @@ sig
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
-    CicAst.term ->
+    DisambiguateTypes.term ->
     (DisambiguateTypes.environment * (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
@@ -51,7 +51,7 @@ sig
     dbd:Mysql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    TacticAst.obj ->
+    GrafiteAst.obj ->
     (DisambiguateTypes.environment * (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -79,3 +79,6 @@ sig
      Cic.term *
      CicUniv.universe_graph) list   (* disambiguated term *)
 end
+
+val dummy_floc: Lexing.position * Lexing.position
+