X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.mli;h=6f74c23c0ab674bcf213a60992e4544c0574ff55;hb=206f96afb7097c20b3cc8bd144825467b4fde7ae;hp=ca33fa4226db2cdd4c667b1090692eb43634faa6;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index ca33fa422..6f74c23c0 100644
--- 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
+