diff options
| author | Hugo Herbelin | 2014-08-14 20:44:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:38 +0200 |
| commit | d5fece25d8964d5d9fcd55b66164286aeef5fb9f (patch) | |
| tree | 60d584831ef3574c8d07daaef85929bd81a12d88 /plugins/funind/functional_principles_proofs.ml | |
| parent | 4684ae383a6ee56b4717026479eceb3b41b45ab0 (diff) | |
Reorganization of tactics:
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 1981fb837b..7f0db547d3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1433,11 +1433,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = backtrack_eqs_until_hrec hrec eqs; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) (tclTHENS (* We must have exactly ONE subgoal !*) - (apply (mkVar hrec)) + (Proofview.V82.of_tactic (apply (mkVar hrec))) [ tclTHENSEQ [ keep (tcc_hyps@eqs); - apply (Lazy.force acc_inv); + (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); (fun g -> if is_mes then @@ -1556,7 +1556,7 @@ let prove_principle_for_gen ( (* observe_tac *) (* "apply wf_thm" *) - Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])) + Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))) ) ) ) |