-
Guillaume Melquiond authored
When a mlw file contained "while not foo do", one of the VCs contained "not not foo" as a hypothesis, due to a poor interaction between bool and prop. This commit ensures that such hypotheses get simplified to "foo".
91961ccd