exception IncludedFileNotCompiled of string
type statement =
- (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
+ (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+ string)
+ GrafiteAst.statement
(* heavy checks slow down the compilation process but give you some interesting
* infos like if the theorem is a duplicate *)