Parsers.EntrySourcetype test = | Convert of Kernel.Term.term * Kernel.Term.termConvertibility between the two given terms.
*)| HasType of Kernel.Term.term * Kernel.Term.termTypability test, given a term and a type.
*)Possible tests in source files.
type entry = | Decl of Kernel.Basic.loc
* Kernel.Basic.ident
* Kernel.Signature.scope
* Kernel.Signature.staticity
* Kernel.Term.termSymbol declaration.
*)| Def of Kernel.Basic.loc
* Kernel.Basic.ident
* Kernel.Signature.scope
* is_opaque
* Kernel.Term.term option
* Kernel.Term.termDefinition (possibly opaque).
*)| Rules of Kernel.Basic.loc * Kernel.Rule.partially_typed_rule listReduction rules declaration.
*)| Eval of Kernel.Basic.loc * Kernel.Reduction.red_cfg * Kernel.Term.termEvaluation command.
*)| Check of Kernel.Basic.loc * is_assertion * should_fail * testTest command.
*)| Infer of Kernel.Basic.loc * Kernel.Reduction.red_cfg * Kernel.Term.termType inference command.
*)| Print of Kernel.Basic.loc * stringPrinting command.
*)| DTree of Kernel.Basic.loc * Kernel.Basic.mident option * Kernel.Basic.identDecision tree printing.
*)| Name of Kernel.Basic.loc * Kernel.Basic.mident| Require of Kernel.Basic.loc * Kernel.Basic.midentRequire command.
*)Single source file entry.