diff options
| author | Pierre-Marie Pédrot | 2016-10-18 10:34:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-18 10:34:23 +0200 |
| commit | dff1450d43909e8aeaf8ce2db8bc19be42ee1ab1 (patch) | |
| tree | dc76cb36c6fd8db422595d9134b3bd45b971462d /pretyping/evarconv.ml | |
| parent | 62fd23efbb4de5415c021dca37ed9f7b4be99729 (diff) | |
| parent | 317ae3b327d201530730ed2cce5f44e8763814d4 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 73f2512431..3680cd777a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1147,7 +1147,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 -> + | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) |