exception BaseUriNotSetYet
-(*
-type tactic =
- (NotationPt.term, NotationPt.term,
- NotationPt.term GrafiteAst.reduction, string)
- GrafiteAst.tactic *)
-
-val disambiguate_command:
- LexiconEngine.status as 'status ->
- ?baseuri:string ->
- GrafiteAst.command Disambiguate.disambiguator_input ->
- 'status * GrafiteAst.command
+class type g_status =
+ object
+ inherit LexiconTypes.g_status
+ inherit NCicCoercion.g_status
+ end
+
+class status :
+ object ('self)
+ inherit LexiconTypes.status
+ inherit NCicCoercion.status
+ method set_grafite_disambiguate_status: #g_status -> 'self
+ end
val disambiguate_nterm :
NCic.term option ->
- (#NEstatus.status as 'status) ->
+ (#status as 'status) ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
- #NEstatus.status as 'status ->
+ #status as 'status ->
?baseuri:string ->
(NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
'status * NCic.obj
val disambiguate_npattern:
GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-
-