|Page 762 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Unknown unitac operator in root of argumentation: t
During tactic expansion of the unification tactic , the unification tactic does unitac expansion of x. During this unitac expansion, the unitac evaluator encountered an operator which was not a unitac tactic. The error message contains the entire term t which cannot be unitac 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 762 of 800||Search logiweb.eu|