diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-30 18:45:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-30 18:45:55 +0000 |
| commit | a9ecb7e57fed81f936045f30830322834f95a17e (patch) | |
| tree | 3fec931b526937aa4e85c4ccff4b873ffe3aa01f /checker/reduction.ml | |
| parent | 13cab8364beb03586e0e6972f00c20664d83a4b7 (diff) | |
Continuation of r16346 on filtering local definitions. Refined
the "choose less dependent" constraint-solving heuristic so that
it is not disturbed by local definitions.
This is a quick fix. A deeper analysis of the structure of constraints
of the form ?x[args] = y, determining if variable y can itself be a
local def or not, and whether args can be let-ins aliasing other
variables, would allow to know if the fix needs to be refined further.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/reduction.ml')
0 files changed, 0 insertions, 0 deletions