From 8613255ff2cc553ec7e8a2fd774e51fc881f712d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Sep 2018 18:47:40 -0700 Subject: [PATCH] chore(library/compiler/csimp): add comment --- src/library/compiler/csimp.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index c89b6b8725..d5d842ee14 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -328,7 +328,9 @@ class csimp_fn { return some_expr(mk_app(fn, args)); } } else { - /* Create jp value */ + /* Create jp value for `e` + This kind of join-point is not very useful. It will only help if we decide + to inline the join-point later in some of the branches. */ local_decl fvar_decl = m_lctx.get_local_decl(fvar); expr jp_val = e; {