- coercion now requires an URI

[helm.git] / helm / ocaml / grafite_parser / grafiteDisambiguate.mli

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
index 21836853f05aec0108b30c39879a837168abdedb..379b65c1e17d39ae5dc0736a2fbf19c448ef1ef6 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
@@ -32,5 +32,6 @@ val disambiguate_tactic:
 
 val disambiguate_command: 
  GrafiteTypes.status ->
-  (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command ->
-  GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command
+  CicNotationPt.obj GrafiteAst.command ->
+  GrafiteTypes.status * Cic.obj GrafiteAst.command
+