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/invfun.ml | |
| parent | 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (diff) | |
More conversion functions in the new tactic API.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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 |