diff options
| author | Pierre-Marie Pédrot | 2016-11-25 11:36:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:39 +0100 |
| commit | 778e863b77bcafc8ed339dd02226e85e5fee2532 (patch) | |
| tree | c836854265a6c1ac401b524710a0b7947bea3d37 /pretyping | |
| parent | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (diff) | |
Removing compatibility layers related to printing.
Diffstat (limited to 'pretyping')
| -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 afb0bf6d5a..87267d5389 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -385,7 +385,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) - let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in + let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem on_left pbty,ev,t2) |