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/ssr | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
Merge PR #6831: [located] More work towards using CAst.t
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 2bed8b624b..2f8b8cb02c 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -541,7 +541,7 @@ END (* ipats *) -let remove_loc = snd +let remove_loc x = x.CAst.v let ipat_of_intro_pattern p = Misctypes.( let rec ipat_of_intro_pattern = function @@ -608,14 +608,15 @@ let interp_intro_pattern = interp_wit wit_intro_pattern let interp_introid ist gl id = Misctypes.( try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) - with _ -> snd(snd (interp_intro_pattern ist gl (Loc.tag @@ IntroNaming (IntroIdentifier id)))) + with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v ) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps (loc, ipat) hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = Misctypes.( + let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> if not_section_id id then SsrHyp (loc, id) :: hyps else @@ -646,7 +647,7 @@ let interp_ipat ist gl = | IPatClear clr -> let add_hyps (SsrHyp (loc, id) as hyp) hyps = if not (ltacvar id) then hyp :: hyps else - add_intro_pattern_hyps (loc, (interp_introid ist gl id)) hyps in + add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in check_hyps_uniq [] clr'; IPatClear clr' | IPatCase(iorpat) -> |