diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-08 18:32:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-08 19:05:14 +0100 |
| commit | bf388dfec041ab0fa74ae5d484600f6fcf515e4f (patch) | |
| tree | 4e62fb2fc2fdc58f740dbe17eabb1e3883dc42a9 | |
| parent | d08532d5344d96d10604760fa44109c9d56e73ce (diff) | |
Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt 8.4.
| -rw-r--r-- | pretyping/evarsolve.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 078117fbd..f5d8baed9 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1104,14 +1104,7 @@ let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) = let opp_problem = function None -> None | Some b -> Some (not b) -let preferred_orientation evd evk1 evk2 = - let _,src1 = (Evd.find_undefined evd evk1).evar_source in - let _,src2 = (Evd.find_undefined evd evk2).evar_source in - (* This is a heuristic useful for program to work *) - match src1,src2 with - | Evar_kinds.QuestionMark _, _ -> true - | _,Evar_kinds.QuestionMark _ -> false - | _ -> true +let preferred_orientation evd evk1 evk2 = false let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env in |