From ec7ff743b42e9549519d556d36cf770802a6912f Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 27 Nov 2018 14:41:22 -0800
Subject: Treat unmatched goals as new for diffs (highlighted) Improve debug
 output

---
 ide/idetop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index a2b85041e8..ea7c208314 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -219,7 +219,7 @@ let goals () =
         | Some oldp ->
           let (_,_,_,_,osigma) = Proof.proof oldp in
           (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
-          with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)"))
+          with Not_found -> None) (* will appear as a new goal *)
         | None -> None
         in
         let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
-- 
cgit v1.2.3