Rephrasing comments.
This commit is contained in:
parent
5608b29dc0
commit
ccae884942
@ -353,14 +353,14 @@ so technically this is a bug. Don't use.
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Check for c-minimality
|
// Check for redundant patterns
|
||||||
{
|
{
|
||||||
if (!non_redundant ())
|
if (!non_redundant ())
|
||||||
{
|
{
|
||||||
if (switches.output == PROOF)
|
if (switches.output == PROOF)
|
||||||
{
|
{
|
||||||
indentPrint ();
|
indentPrint ();
|
||||||
eprintf ("Pruned because this is not <=c-minimal.\n");
|
eprintf ("Pruned because the pattern is redundant.\n");
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user