From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- proofs/proof_type.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'proofs/proof_type.ml') 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) -- cgit v1.2.3