Huge reorganization of matita and ocaml.

[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 379b65c1e17d39ae5dc0736a2fbf19c448ef1ef6..9944825e66f9e32288af34d718c58d8b7f865e25 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
@@ -23,15 +23,19 @@
  * http://helm.cs.unibo.it/
  *)
 
+exception BaseUriNotSetYet
+
 val disambiguate_tactic:
- GrafiteTypes.status ->
- ProofEngineTypes.goal ->
+ LexiconEngine.status ref ->
+ Cic.context ->
+ Cic.metasenv ->
  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic ->
- GrafiteTypes.status ref *
-  (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
+  Cic.metasenv *
+   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
 
 val disambiguate_command: 
- GrafiteTypes.status ->
+ LexiconEngine.status ->
+ baseuri:string option ->
+ Cic.metasenv ->
   CicNotationPt.obj GrafiteAst.command ->
-  GrafiteTypes.status * Cic.obj GrafiteAst.command
-
+  LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command