incr next_id;
!next_id
in
- let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ, attrs) 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 attrs = let (_, _, _, _, attrs) = _proof in attrs
+ 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, attes) = _proof in
- _proof <- (uri, metasenv, body, typ, attrs)
+ 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, attrs) = _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, attrs)
+ _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 =