|Page 751 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Unknown tactic operator in root of argumentation: t
During tactic expansion, the tactic evaluator encountered an operator which was not a tactic. The error message contains the entire term t which cannot be tactic expanded. The problematic operator is the principal operator of t.
The term t is given out of context and after macro expansion, so start out by locating the error.
|Page 751 of 800||Search logiweb.eu|