- | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl
- | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl
- | "destructions" :: tl -> k ok ("destructions" :: outs) tl
- | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl
- | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl
- | "inversions" :: tl -> k ok ("inversions" :: outs) tl
- | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl
- | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl
- | "constructions" :: tl -> k ok ("constructions" :: outs) tl
- | "properties" :: tl -> k ok ("constructions" :: outs) tl
- | _ -> k true outs ins
+ | "iterators" :: tl -> k T.OK ("iterators" :: outs) tl
+ | "eliminations" :: tl -> k T.OK ("eliminations" :: outs) tl
+ | "eliminators" :: tl -> k T.OK ("eliminations" :: outs) tl
+ | "equalities" :: tl -> k T.OK ("equalities" :: outs) tl
+ | "destructions" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "forward" :: "properties" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "forward" :: "lemmas" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "inversions" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: "properties" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: "lemmas" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "constructions" :: tl -> k T.OK ("constructions" :: outs) tl
+ | "properties" :: tl -> k T.OK ("constructions" :: outs) tl
+ | _ -> k T.KO outs ins