diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 74affa3964..5cee3cb204 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -871,10 +871,10 @@ let rec make_rewrite_list expr_info max = function in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true - (mkVar hp, + (EConstr.mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S max)]) false) g) ) + EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k, + EConstr.of_constr (f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -898,10 +898,10 @@ let make_rewrite expr_info l hp max = observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true - (mkVar hp, + (EConstr.mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S (f_S max))]) false)) g) + EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k, + EConstr.of_constr (f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ |