diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 16 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
4 files changed, 15 insertions, 15 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' -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d1e109825..41fd0bd18 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -113,7 +113,7 @@ let functional_induction with_clean c princl pat = in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) - (Tactics.reduce flag Locusops.allHypsAndConcl) + (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) g else Tacticals.tclIDTAC g in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ae2091a22..2b45206bb 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -363,14 +363,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false ; Genredexpr.rConst = [] } ) - Locusops.onConcl; + Locusops.onConcl); observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -532,12 +532,12 @@ and intros_with_rewrite_aux : tactic = ] g | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -547,12 +547,12 @@ and intros_with_rewrite_aux : tactic = end | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -692,12 +692,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; generalize (List.map mkVar ids); thin ids diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 834d0acea..6c6caa628 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -562,7 +562,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = observe_tclTHENLIST (str "destruct_bounds_aux2")[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; - observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); + observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); observe_tac (str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)])); @@ -902,7 +902,7 @@ let make_rewrite expr_info l hp max = [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ - simpl_iter Locusops.onConcl; + Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)])); |