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.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index dbe40780..41935c9c 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *) +(*i $Id: proof_type.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (*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 @@ -94,3 +93,16 @@ and 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 + +let abstract_tactic_box = ref (ref None) |