Split IsPure into IntoPure and FromPure.

This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.
1 job for master
Status Job ID Name Coverage
  Test
passed #490
coq
buildjob

00:03:50