- |GrafiteAst.Assume (_,id,t,t1) -> Declarative.assume id (text,prefix_len,t) (match t1 with None ->
- None | Some t1 -> (Some (text,prefix_len,t1)))
- |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose (text,prefix_len,t) id (match t1 with None
- -> None | Some t1 -> (Some (text,prefix_len,t1)))
- |GrafiteAst.By_just_we_proved (_,j,t1,s,t2) -> Declarative.by_just_we_proved
- (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s (match t2 with None -> None |
- Some t2 -> (Some (text,prefix_len,t2)))
- |GrafiteAst.We_need_to_prove (_, t, id, t1) -> Declarative.we_need_to_prove (text,prefix_len,t) id
- (match t1 with None -> None | Some t1 -> Some (text,prefix_len,t1))
+ |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t)
+ |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id
+ |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved
+ (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s
+ |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id