diff options
| -rw-r--r-- | proofs/proofview.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index e19236df04..a30175de1a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -162,8 +162,7 @@ let focus i j sp = ( { sp with comb = new_comb } , context ) (* Unfocuses a proofview with respect to a context. *) -let undefined defs l = - Option.List.flatten (List.map (Goal.advance defs) l) +let undefined defs l = CList.map_filter (Goal.advance defs) l let unfocus c sp = { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } |