diff options
| author | Pierre-Marie Pédrot | 2014-08-23 01:11:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-23 01:12:11 +0200 |
| commit | a8f63f0dd852bf4510111feaf8bcdb7b4869c64d (patch) | |
| tree | aed95dd5d4b5bed8f8874d516a24e727c32e72c5 /doc/tutorial/Tutorial.tex | |
| parent | 47fbb3a74b9bd52b19e63e695fb1902ed345488e (diff) | |
Fixing bug #3533.
Now error printing tries to set universe printing when two terms are not
desambiguated.
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
0 files changed, 0 insertions, 0 deletions