diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 10 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 35 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 38 |
3 files changed, 83 insertions, 0 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli new file mode 100644 index 000000000..7b3d05eeb --- /dev/null +++ b/proofs/pfedit.mli @@ -0,0 +1,10 @@ + +(* $Id$ *) + +(*i*) +open Pp +(*i*) + +val proof_prompt : unit -> string +val refining : unit -> bool +val msg_proofs : bool -> std_ppcmds diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml new file mode 100644 index 000000000..77e8314d5 --- /dev/null +++ b/proofs/proof_trees.ml @@ -0,0 +1,35 @@ + +(* $Id$ *) + +open Term + +type bindOcc = + | Dep of identifier + | NoDep of int + | Com + +type 'a substitution = (bindOcc * 'a) list + +type tactic_arg = + | COMMAND of Coqast.t + | CONSTR of constr + | IDENTIFIER of identifier + | INTEGER of int + | CLAUSE of identifier list + | BINDINGS of Coqast.t substitution + | CBINDINGS of constr substitution + | QUOTED_STRING of string + | TACEXP of Coqast.t + | REDEXP of string * Coqast.t list + | FIXEXP of identifier * int * Coqast.t + | COFIXEXP of identifier * Coqast.t + | LETPATTERNS of int list option * (identifier * int list) list + | INTROPATTERN of intro_pattern + +and intro_pattern = + | IdPat of identifier + | DisjPat of intro_pattern list + | ConjPat of intro_pattern list + | ListPat of intro_pattern list + +and tactic_expression = string * tactic_arg list diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli new file mode 100644 index 000000000..99d94d01e --- /dev/null +++ b/proofs/proof_trees.mli @@ -0,0 +1,38 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +(*i*) + +type bindOcc = + | Dep of identifier + | NoDep of int + | Com + +type 'a substitution = (bindOcc * 'a) list + +type tactic_arg = + | COMMAND of Coqast.t + | CONSTR of constr + | IDENTIFIER of identifier + | INTEGER of int + | CLAUSE of identifier list + | BINDINGS of Coqast.t substitution + | CBINDINGS of constr substitution + | QUOTED_STRING of string + | TACEXP of Coqast.t + | REDEXP of string * Coqast.t list + | FIXEXP of identifier * int * Coqast.t + | COFIXEXP of identifier * Coqast.t + | LETPATTERNS of int list option * (identifier * int list) list + | INTROPATTERN of intro_pattern + +and intro_pattern = + | IdPat of identifier + | DisjPat of intro_pattern list + | ConjPat of intro_pattern list + | ListPat of intro_pattern list + +and tactic_expression = string * tactic_arg list |