- (** TODO Zack to be reviewed and unified with proof_viewer above *)
-class type sequent_viewer =
- object
- inherit GMathViewAux.multi_selection_math_view
-
- (** @return the list of selected terms. Selections which are not terms are
- * ignored *)
- method get_selected_terms: Cic.term list
-
- (** @return the list of selected hypothese. Selections which are not
- * hypotheses are ignored *)
- method get_selected_hypotheses: Cic.hypothesis list
-
- (** load a sequent and render it into parent widget *)
- method load_sequent: Cic.metasenv -> Cic.conjecture -> unit
- end
-
-class type proof_viewer =
- object
- inherit GMathViewAux.single_selection_math_view
-
- (** @return the annotated cic term and the ids_to_inner_types and
- * ids_to_inner_sorts maps *)
- method load_proof: Gdome.document -> hist_metadata -> unit
-
- end
-
-(** {2 shorthands} *)
-