diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /proofs/decl_expr.mli | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'proofs/decl_expr.mli')
-rw-r--r-- | proofs/decl_expr.mli | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli new file mode 100644 index 00000000..24af3842 --- /dev/null +++ b/proofs/decl_expr.mli @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Util +open Tacexpr + +type ('constr,'tac) justification = + By_tactic of 'tac +| Automated of 'constr list + +type 'it statement = + {st_label:name; + st_it:'it} + +type thesis_kind = + Plain + | Sub of int + | For of identifier + +type 'this or_thesis = + This of 'this + | Thesis of thesis_kind + +type side = Lhs | Rhs + +type elim_type = + ET_Case_analysis + | ET_Induction + +type block_type = + B_proof + | B_claim + | B_focus + | B_elim of elim_type + +type ('it,'constr,'tac) cut = + {cut_stat: 'it statement; + cut_by: ('constr,'tac) justification} + +type ('var,'constr) hyp = + Hvar of 'var + | Hprop of 'constr statement + +type ('constr,'tac) casee = + Real of 'constr + | Virtual of ('constr,'constr,'tac) cut + +type ('hyp,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pcut of ('constr or_thesis,'constr,'tac) cut + | Prew of side * ('constr,'constr,'tac) cut + | Passume of ('hyp,'constr) hyp list + | Plet of ('hyp,'constr) hyp list + | Pgiven of ('hyp,'constr) hyp list + | Pconsider of 'constr*('hyp,'constr) hyp list + | Pclaim of 'constr statement + | Pfocus of 'constr statement + | Pdefine of identifier * 'hyp list * 'constr + | Pcast of identifier or_thesis * 'constr + | Psuppose of ('hyp,'constr) hyp list + | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Ptake of 'constr list + | Pper of elim_type * ('constr,'tac) casee + | Pend of block_type + | Pescape + +type emphasis = int + +type ('hyp,'constr,'pat,'tac) gen_proof_instr= + {emph: emphasis; + instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + + +type raw_proof_instr = + ((identifier*(Topconstr.constr_expr option)) located, + Topconstr.constr_expr, + Topconstr.cases_pattern_expr, + raw_tactic_expr) gen_proof_instr + +type glob_proof_instr = + ((identifier*(Genarg.rawconstr_and_expr option)) located, + Genarg.rawconstr_and_expr, + Topconstr.cases_pattern_expr, + Tacexpr.glob_tactic_expr) gen_proof_instr + +type proof_pattern = + {pat_vars: Term.types statement list; + pat_aliases: (Term.constr*Term.types) statement list; + pat_constr: Term.constr; + pat_typ: Term.types; + pat_pat: Rawterm.cases_pattern; + pat_expr: Topconstr.cases_pattern_expr} + +type proof_instr = + (Term.constr statement, + Term.constr, + proof_pattern, + Tacexpr.glob_tactic_expr) gen_proof_instr |