X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.mli;h=123fcf96928f82fd10f0f43cb3d26b3b30648450;hb=e9bc7577856e02545d3bc84d8f20aa15c5842034;hp=021fe1c9d676bb59a9a7cfcd6fbc93bcbaa0e35a;hpb=45ac0bf0fb6c58e03646588d4f81cf5125058e67;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 021fe1c9d..123fcf969 100644
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -73,7 +73,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj disambiguator_input ->
+    CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *