Page 762 of 800
| 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 |