diff options
| author | filliatr | 1999-09-28 14:40:28 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-28 14:40:28 +0000 |
| commit | 3637df25c6201e7c593472798689edab656bab6d (patch) | |
| tree | c69c4c32c651681c30f85f114575ea92086e7a1d | |
| parent | f43e3118c01218d1de6924ed6825897eeca5bcf3 (diff) | |
quelques trucs necessaires au toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@84 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 0000000000..7b3d05eeb4 --- /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 0000000000..77e8314d5f --- /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 0000000000..99d94d01e3 --- /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 |