summaryrefslogtreecommitdiff
path: root/proofs/refiner.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /proofs/refiner.mli
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'proofs/refiner.mli')
-rw-r--r--proofs/refiner.mli32
1 files changed, 22 insertions, 10 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 417ddbcd..d8b13dba 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: refiner.mli 7911 2006-01-21 11:18:36Z herbelin $ i*)
+(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*)
(*i*)
open Term
@@ -32,20 +32,17 @@ val apply_sig_tac :
type transformation_tactic = proof_tree -> (goal list * validation)
-val add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
-val lookup_tactic : string -> (closed_generic_argument list) -> tactic
-
(*s Hiding the implementation of tactics. *)
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
- a single proof node *)
-val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : tactic_expr -> tactic -> tactic
-val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+ a single proof node. The boolean tells if the default tactic is used. *)
+val abstract_operation : compound_rule -> tactic -> tactic
+val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
+val abstract_extended_tactic :
+ ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
val refiner : rule -> tactic
-val vernac_tactic : string * closed_generic_argument list -> tactic
val frontier : transformation_tactic
val list_pf : proof_tree -> goal list
val unTAC : tactic -> goal sigma -> proof_tree sigma
@@ -148,6 +145,12 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
+(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
+ has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
+ Equivalent to [(tac1;try tac2)||tac2] *)
+
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
+
(*s Tactics handling a list of goals. *)
type validation_list = proof_tree list -> proof_tree list
@@ -170,11 +173,14 @@ type pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
+val match_rule : (rule -> bool) -> pftreestate -> bool
val evc_of_pftreestate : pftreestate -> evar_map
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
+val map_pftreestate :
+ (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
@@ -193,6 +199,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate
val next_unproven : pftreestate -> pftreestate
val prev_unproven : pftreestate -> pftreestate
val top_of_tree : pftreestate -> pftreestate
+val match_rule : (rule -> bool) -> pftreestate -> bool
+val up_until_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val up_to_matching_rule : (rule -> bool) ->
+ pftreestate -> pftreestate
+val change_rule : (rule -> rule) -> pftreestate -> pftreestate
val change_constraints_pftreestate
: evar_map -> pftreestate -> pftreestate