1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: proof_search.mli 7233 2005-07-15 12:34:56Z corbinea $ *)
13
| Arrow of form * form
15
| Conjunct of form * form
16
| Disjunct of form * form
21
| E_Arrow of int*int*proof
22
| D_Arrow of int*proof*proof
24
| I_And of proof*proof
29
| E_Or of int*proof*proof
35
val project: state -> proof
37
val init_state : ('a * form * 'b) list -> form -> state
39
val branching: state -> state list
41
val success: state -> bool
45
val pr_form : form -> unit
47
val reset_info : unit -> unit
49
val pp_info : unit -> unit