diff options
| author | herbelin | 2013-03-30 18:45:55 +0000 |
|---|---|---|
| committer | herbelin | 2013-03-30 18:45:55 +0000 |
| commit | a9ecb7e57fed81f936045f30830322834f95a17e (patch) | |
| tree | 3fec931b526937aa4e85c4ccff4b873ffe3aa01f /pretyping/evarconv.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 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2d21fb0e77..8da09d5c56 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -782,14 +782,16 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let app_empty = match l1, l2 with [], [] -> true | _ -> false in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty - && Array.for_all (fun a -> eq_constr a term2 || isEvar a) args1 -> + & List.for_all (fun a -> eq_constr a term2 or isEvar a) + (remove_instance_local_defs evd evk1 (Array.to_list args1)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) | (Rel _|Var _), Evar (evk2,args2) when app_empty - & Array.for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> + & List.for_all (fun a -> eq_constr a term1 or isEvar a) + (remove_instance_local_defs evd evk2 (Array.to_list args2)) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with |