diff options
| author | Hugo Herbelin | 2018-12-12 23:41:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-12 23:41:11 +0100 |
| commit | 4ecbad30c77316294c8625ead722d469c1c7f79d (patch) | |
| tree | 5cb1d9e2d15149dfa4ee570bf8b78d03bf235723 /ide | |
| parent | bb10141086110b8a736eb1e54292e5a48764f519 (diff) | |
| parent | c6b7a288eb9173b4b1c9df67230449fde42b9210 (diff) | |
Merge PR #9101: Fix 8922 again
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 8b3b566f9c..6a4c7603ee 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 |