diff options
| author | Pierre-Marie Pédrot | 2014-03-26 20:37:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-26 20:42:26 +0100 |
| commit | 73ddce3136549532c81405fa82871dcd3a51b28f (patch) | |
| tree | 8cdba08a62187f03cd3096e61f1976bf0e7a30c0 /toplevel | |
| parent | 681fe91e80266c0947f0fad72e6f509d75ea34f9 (diff) | |
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 94447f0d04..253d218988 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -378,7 +378,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (Tactics.emit_side_effects eff); + Proofview.tclEFFECTS eff; Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto] end @@ -448,7 +448,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt = then bl_t1 else mkApp (bl_t1,bl_args) in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (Tactics.emit_side_effects eff) ; + Proofview.tclEFFECTS eff; Equality.replace_by t1 t2 (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply app)) (Auto.default_auto)) ; aux q1 q2 ] @@ -861,10 +861,9 @@ let compute_dec_tact ind lnamesparrec nparrec = Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++ str" equality is required.")) end >>= fun (lbI,eff'') -> + let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (Tactics.emit_side_effects - (Declareops.union_side_effects eff'' - (Declareops.union_side_effects eff' eff))); + Proofview.tclEFFECTS eff; intros_using fresh_first_intros; intros_using [freshn;freshm]; (*we do this so we don't have to prove the same goal twice *) |