diff options
| author | Lasse Blaauwbroek | 2020-12-22 07:30:30 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-12-27 18:26:29 +0100 |
| commit | 857f8403fcd216d28bf06d18c2774887ccf8bda5 (patch) | |
| tree | 3393c2cc3e0da7bbe9b29c783e6da2963b1186be /plugins/ssr | |
| parent | d1af000c4b9b1d1ff9b2f9fbf2dcb570ae7c974c (diff) | |
Refactor cpattern into a record
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrbwd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 0f10183426..37eba7d399 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -123,7 +123,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars: let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then - let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in + let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[]))) else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in tclGENTAC (fun gl -> |