diff options
Diffstat (limited to 'contrib/first-order/sequent.ml')
| -rw-r--r-- | contrib/first-order/sequent.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 91a8f1ddd8..c63c10f43a 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -169,7 +169,16 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup item seq=History.mem item seq.history +let lookup item seq= + History.mem item seq.history || + match item with + (_,None)->false + | (id,Some ((m,t) as c))-> + let p (id2,o)= + match o with + None -> false + | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + History.exists p seq.history let add_left (nam,t) seq internal gl= match build_left_entry nam t internal gl seq.cnt with |