Turn Coq quantifiers into proofmode quantifiers on `iStartProof`
For example, it should turn the Coq goal forall x, P ⊢ Q
into a proof mode goal ∀ x, P → Q
. (And likewise for let-bindings).
Since issue came up in d7db5250, which changes the behavior of iStartProof PROP
, to just introduce all quantifiers. @jjourdan introduced that because in iGPS they were often doing:
intros; iStartProof (uPred _); iIntros (V) "..."
The proposal in this issue fixes this problem in a nicer way.