diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-05 13:56:22 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-05 14:04:03 +0100 |
commit | e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 (patch) | |
tree | 173fdd6bcb0d258985ffcdd125fcef0551dcb822 /proofs/proof_type.ml | |
parent | c7026ec14f94875fc4b58951fa8bec628fcfac42 (diff) |
Respect the transparent state of the current conversion on strong weak-head.
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
Diffstat (limited to 'proofs/proof_type.ml')
0 files changed, 0 insertions, 0 deletions