diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 4fbcda4c..a7057a7d 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli 9842 2007-05-20 17:44:23Z herbelin $ i*) +(*i $Id: proof_type.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Environ @@ -28,8 +28,7 @@ open Pattern type prim_rule = | Intro of identifier - | Intro_replacing of identifier - | Cut of bool * identifier * types + | Cut of bool * bool * identifier * types | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr @@ -37,7 +36,7 @@ type prim_rule = | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list - | Move of bool * identifier * identifier + | Move of bool * identifier * identifier move_location | Rename of identifier * identifier | Change_evars @@ -128,3 +127,17 @@ and tactic_arg = Tacexpr.gen_tactic_arg type hyp_location = identifier Tacexpr.raw_hyp_location + +type ltac_call_kind = + | LtacNotationCall of string + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref + | LtacVarCall of identifier * glob_tactic_expr + | LtacConstrInterp of rawconstr * + ((identifier * constr) list * (identifier * identifier option) list) + +type ltac_trace = (loc * ltac_call_kind) list + +exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn + +val abstract_tactic_box : atomic_tactic_expr option ref ref |