diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 20:04:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 20:04:43 +0000 |
| commit | 7d46472d5e06d78e75646da8b26ee19b3914d36f (patch) | |
| tree | 2fe497887becaa4f1dd170f8e100b76d71a739da | |
| parent | 110db6ddf023c98a76c719caf602559942ba089e (diff) | |
Correction d'un bug dans l'analyse des contraintes non résolues
(report de 11190 de v8.2 vers trunk). Le code fautif n'était en fait
plus utilisé car les contraintes de la forme ?n[..,x,..,x,..] := x que
ce code analysait sont finalement résolues par une heuristique de
consider_remaining_univ_constraints consistant à reproduire le
comportement de la 8.1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11192 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 17 |
2 files changed, 3 insertions, 18 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0fdad5830..1463901a5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -515,12 +515,12 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 = let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] -> - (* The typical kind of constraint coming from patter-matching return + (* The typical kind of constraint coming from pattern-matching return type inference *) assert (array_for_all (fun a -> a = term2 or isEvar a) args1); choose_less_dependent_instance evk1 evd term2 args1, true | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> - (* The typical kind of constraint coming from patter-matching return + (* The typical kind of constraint coming from pattern-matching return type inference *) assert (array_for_all ((=) term1) args2); choose_less_dependent_instance evk2 evd term1 args2, true diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 778fb3f0e..870debaa7 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1057,22 +1057,7 @@ let check_evars env initial_sigma evd c = if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk evd in let evi = nf_evar_info sigma (Evd.find sigma evk) in - let explain = - let f (_,_,t1,t2) = - (try head_evar t1 = evk with Failure _ -> false) - or (try head_evar t2 = evk with Failure _ -> false) in - let check_several c inst = - let _,argsv = destEvar c in - let l = List.filter (eq_constr inst) (Array.to_list argsv) in - let n = List.length l in - (* Maybe should we select one instead of failing ... *) - if n >= 2 then Some (SeveralInstancesFound n) else None in - match List.filter f (snd (extract_all_conv_pbs evd)) with - | (_,_,t1,t2)::_ -> - if isEvar t2 then check_several t2 t1 - else check_several t1 t2 - | [] -> None - in error_unsolvable_implicit loc env sigma evi k explain + error_unsolvable_implicit loc env sigma evi k None | _ -> iter_constr proc_rec c in proc_rec c |