diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /proofs/proof_type.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 |