Comment by manyoso

But Coq is strongly normalizing… it always halts. What gives?