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 /pretyping/evarutil.mli | |
| 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 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 92e819381..4db6fdd3e 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -195,5 +195,3 @@ val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list * constr list val generalize_evar_over_rels : evar_map -> existential -> types * constr list - - |