diff options
Diffstat (limited to 'proofs/decl_expr.mli')
-rw-r--r-- | proofs/decl_expr.mli | 105 |
1 files changed, 0 insertions, 105 deletions
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli deleted file mode 100644 index 5c069cdd..00000000 --- a/proofs/decl_expr.mli +++ /dev/null @@ -1,105 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: decl_expr.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - -open Names -open Util -open Tacexpr - -type 'it statement = - {st_label:name; - st_it:'it} - -type thesis_kind = - Plain - | 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; - cut_by: 'constr list option; - cut_using: 'tac option} - -type ('var,'constr) hyp = - Hvar of 'var - | Hprop of 'constr statement - -type ('constr,'tac) casee = - Real of 'constr - | Virtual of ('constr statement,'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 statement,'constr,'tac) cut - | Prew of side * ('constr statement,'constr,'tac) cut - | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'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 |