X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=b04aa3cde54530fea0e1c1419a9cda97aa8c9bb8;hb=742332c845b599fbdaa86a02e21a5f223a4783f9;hp=379b65c1e17d39ae5dc0736a2fbf19c448ef1ef6;hpb=7a7af8e1ed42aa440476975ec918d38f0c3d13c9;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
index 379b65c1e..b04aa3cde 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
@@ -23,15 +23,26 @@
  * 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
 
+val disambiguate_macro:
+ LexiconEngine.status ref ->
+ Cic.metasenv ->
+ Cic.context ->
+  CicNotationPt.term GrafiteAst.macro ->
+  Cic.metasenv * Cic.term GrafiteAst.macro