diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-09 15:57:37 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:23:29 +0200 |
| commit | 4c339d5e9efce992bae3c88598d04250946fcdd2 (patch) | |
| tree | 35169d0472300053330b81fec8652460ae5f66f4 | |
| parent | ae38a32f1eb7493fed2f4ccca8c4af7c2595a7ac (diff) | |
Proofview: small optimisation/simplification.
| -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 e19236df0..a30175de1 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) } |