diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 15:17:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 15:31:14 +0100 |
| commit | 4ea9b3193eaced958bb277c0723fb54d661ff520 (patch) | |
| tree | 674fe651612dc17f3bf99404fae02d58437ef5a1 /plugins/funind/functional_principles_proofs.ml | |
| parent | 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (diff) | |
More conversion functions in the new tactic API.
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index aa89f89b7..86302dc6c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -371,12 +371,12 @@ let isLetIn t = | _ -> false -let h_reduce_with_zeta = - reduce +let h_reduce_with_zeta cl = + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; - }) + }) cl) @@ -707,7 +707,7 @@ let build_proof [ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [Locus.AllOccurrencesBut [1],t] None; + Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); (fun g' -> |