-class proof: uri:UriManager.uri -> typ:Cic.term ->
- object
- (** {3 status} *)
- method status: proofStatus
- method setStatus: proofStatus -> unit
- end
-
-(** {2 tactic commands builders} *)
-
-(* TODO Zack: these are just some examples, a lot of other tactics/tacticals
- * must be added here *)
-
-val intros: ?namer:MatitaTypes.namer ->
- proofStatus -> MatitaTypes.command
-
-val reflexivity: proofStatus -> MatitaTypes.command
-val symmetry: proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> proofStatus -> MatitaTypes.command
-
-val exists: proofStatus -> MatitaTypes.command
-val split: proofStatus -> MatitaTypes.command
-val left: proofStatus -> MatitaTypes.command
-val right: proofStatus -> MatitaTypes.command
-
-val assumption: proofStatus -> MatitaTypes.command
-