aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 47955e8e0..0fd508604 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -456,7 +456,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Evar must be undefined since we have flushed evars *)
let () = if !debug_unification then
let open Pp in
- pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in
+ pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())
+ ++ fnl ()) in
match (flex_kind_of_term ts env term1 sk1, flex_kind_of_term ts env term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =