diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 19:32:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 19:54:05 +0200 |
| commit | c12e158ad85da9d5e78026997ef6ca969c8ad3a6 (patch) | |
| tree | 270526cfba2ef4913ac5d2bb4c4708f680d6db9b | |
| parent | 35a4b6b66031093497d1f645f6297607155c479d (diff) | |
Fixing a missing constraint in consider_remaining_unif_constraints.
| -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 0d261f7f8..d82d555f8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1130,7 +1130,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let f env evd pbty x y = is_trans_fconv pbty ts 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) |