aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-02 01:15:54 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-02 14:53:27 +0100
commit85ed2504568ee06207546b1ac0660e9c559bca22 (patch)
tree24f5c44a637a7cbeb8e6045c545fd9870f1f88d3 /plugins/firstorder
parente0449b763d5854da2e7e48f4e92da779913a0347 (diff)
Writing [cut] tactic using the new monad.
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/rules.ml6
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e856326c8..fe22708a0 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -141,7 +141,7 @@ let left_instance_tac (inst,id) continue seq=
if lookup (id,None) seq then
tclFAIL 0 (Pp.str "already done")
else
- tclTHENS (cut dom)
+ tclTHENS (Proofview.V82.of_tactic (cut dom))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
(fun gls->generalize
@@ -175,7 +175,7 @@ let left_instance_tac (inst,id) continue seq=
let right_instance_tac inst continue seq=
match inst with
Phantom dom ->
- tclTHENS (cut dom)
+ tclTHENS (Proofview.V82.of_tactic (cut dom))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
(fun gls->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 99e03cdbe..6d9af2bbf 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -144,12 +144,12 @@ let ll_arrow_tac a b c backtrack id continue seq=
mkApp ((constr_of_global id),
[|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclORELSE
- (tclTHENS (cut c)
+ (tclTHENS (Proofview.V82.of_tactic (cut c))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
clear_global id;
wrap 1 false continue seq];
- tclTHENS (cut cc)
+ tclTHENS (Proofview.V82.of_tactic (cut cc))
[exact_no_check (constr_of_global id);
tclTHENLIST
[generalize [d];
@@ -184,7 +184,7 @@ let left_exists_tac ind backtrack id continue seq gls=
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
- (tclTHENS (cut prod)
+ (tclTHENS (Proofview.V82.of_tactic (cut prod))
[tclTHENLIST
[Proofview.V82.of_tactic intro;
(fun gls->