diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-29 05:14:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-29 05:14:44 +0000 |
| commit | c6763b44c75b2bd9aebdbcd0798287c90431cde4 (patch) | |
| tree | 5a04663d2ef32d34fc239a3923a26c6e2ca3d7f0 /lib/fmap.ml | |
| parent | 254da5d698f821172c70899c6a1d95b3b15f8cd8 (diff) | |
Fixing #2836 (materialize_evar might refine as a side effect the
current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/fmap.ml')
0 files changed, 0 insertions, 0 deletions