diff options
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c682829087..efbe2f3358 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -164,10 +164,9 @@ let rec evar_conv_x env evd pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 & - is_fconv pbty env (evars_of evd) term1 term2 + if is_ground_term evd term1 && is_ground_term evd term2 then - (evd,true) + (evd,is_fconv pbty env (evars_of evd) term1 term2) else let term1 = apprec_nohdbeta env evd term1 in let term2 = apprec_nohdbeta env evd term2 in |