-
Ralf Jung authored
* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics * use reduction-controlled `pm_default` for proofmode accessors
3bd43113
* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics * use reduction-controlled `pm_default` for proofmode accessors