diff options
| author | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
| commit | 93a1c4786c9b17efdda025f754ad97376d61a9ba (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /plugins/funind/recdef.ml | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
Merge PR #6831: [located] More work towards using CAst.t
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 759c88633f..4cbcde8e5c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -206,7 +206,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = (RegularStyle,None, [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], DAst.make @@ GVar v_id)]) @@ -899,8 +899,8 @@ let rec make_rewrite_list expr_info max = function Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S max)]) false) g) ) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) @@ -926,8 +926,8 @@ let make_rewrite expr_info l hp max = (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr); - Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ |