-type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-val disambiguate_command:
- LexiconEngine.status as 'status ->
- ?baseuri:string ->
- Cic.metasenv ->
- ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
- 'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
+class type g_status =
+ object
+ inherit LexiconEngine.g_status
+ inherit NCicCoercion.g_status
+ end
+
+class status :
+ object ('self)
+ inherit LexiconEngine.status
+ inherit NCicCoercion.status
+ method set_grafite_disambiguate_status: #g_status -> 'self
+ end