class ['a] status
?(history_size = default_history_size)
- ?uri ~typ ~body ~metasenv init_data compute_data ()
+ ?uri ~typ ~body ~metasenv ~attrs init_data compute_data ()
=
let next_observer_id =
let next_id = ref 0 in
incr next_id;
!next_id
in
- let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ) in
+ let _subst = ([] : Cic.substitution) in
+ let initial_proof = ((uri: UriManager.uri option), metasenv, _subst, body, typ, attrs) in
let next_goal (goals, proof) =
match goals, proof with
| goal :: _, _ -> Some goal
- | [], (_, (goal, _, _) :: _, _, _) ->
+ | [], (_, (goal, _, _) :: _, _, _, _, _) ->
(* the tactic left no open goal: let's choose the first open goal *)
Some goal
| _, _ -> None
raise exn
*)
- method uri = let (uri, _, _, _) = _proof in uri
- method metasenv = let (_, metasenv, _, _) = _proof in metasenv
- method body = let (_, _, body, _) = _proof in body
- method typ = let (_, _, _, typ) = _proof in typ
+ method uri = let (uri, _, _, _, _, _) = _proof in uri
+ method metasenv = let (_, metasenv, _, _, _, _) = _proof in metasenv
+ method body = let (_, _, _, body, _, _) = _proof in body
+ method typ = let (_, _, _, _, typ, _) = _proof in typ
+ method attrs = let (_, _, _, _, _, attrs) = _proof in attrs
method set_metasenv metasenv =
- let (uri, _, body, typ) = _proof in
- _proof <- (uri, metasenv, body, typ)
+ let (uri, _, _subst,body, typ, attes) = _proof in
+ _proof <- (uri, metasenv, _subst,body, typ, attrs)
method set_uri uri =
- let (old_uri, metasenv, body, typ) = _proof in
+ let (old_uri, metasenv, _subst,body, typ, attrs) = _proof in
if old_uri <> None then
raise Uri_redefinition;
- _proof <- (Some uri, metasenv, body, typ)
+ _proof <- (Some uri, metasenv, _subst,body, typ, attrs)
method conjecture goal =
- let (_, metasenv, _, _) = _proof in
+ let (_, metasenv, _subst, _, _, _) = _proof in
CicUtil.lookup_meta goal metasenv
method apply_tactic tactic =
end
-let trivial_status ?uri ~typ ~body ~metasenv () =
- new status ?uri ~typ ~body ~metasenv (fun _ -> ()) (fun _ _ -> ()) ()
+let trivial_status ?uri ~typ ~body ~metasenv ~attrs () =
+ new status ?uri ~typ ~body ~metasenv ~attrs (fun _ -> ()) (fun _ _ -> ()) ()