From 5512bd6d2b8846cdbebfa076815cb0ab817ced50 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 12 Jun 2017 19:00:03 +0200 Subject: [PATCH] minor bug fix --- src/session/session.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/session/session.ml b/src/session/session.ml index 5b643af1a..87b6137db 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -527,8 +527,11 @@ let goal_expl_lazy g = match g.goal_expl with | Some s -> s | None -> - let _name,expl,_task = Termcode.goal_expl_task ~root:false (goal_task g) in - g.goal_expl <- Some expl; expl + match g.goal_task with + | Some t -> + let _name,expl,_task = Termcode.goal_expl_task ~root:false t in + g.goal_expl <- Some expl; expl + | None -> "" let goal_expl_or_name g = let s = goal_expl_lazy g in -- GitLab