diff options
| author | Pierre-Marie Pédrot | 2020-05-01 13:23:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:50 +0200 |
| commit | d6b6d77c4998355bd4db0517f964c9db1937439c (patch) | |
| tree | 2c65a821cbc2186aabc4688b6213634762d43131 /plugins/ssrmatching | |
| parent | 20ee46f95d2198ea32750a7991ec9571c9eb2bb1 (diff) | |
Remove legacy SSR API.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 2 |
2 files changed, 6 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 30957bbc79..adaf7c8cc1 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1224,23 +1224,23 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx -let fill_occ_term env cl occ sigma0 (sigma, t) = +let fill_occ_term env sigma0 cl occ (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with NoMatch -> try let sigma', uc, t' = unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in if sigma' != sigma0 then raise NoMatch - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with _ -> errorstrm (str "partial term " ++ pr_econstr_pat env sigma t ++ str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in - let cl,(_,t) = fill_occ_term env concl occ sigma0 t in + let cl, t = fill_occ_term env sigma0 concl occ t in cl, t let cpattern_of_id id = diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 4a30544a74..17b47227cb 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -191,6 +191,8 @@ val mk_tpattern_matcher : * by [Rel 1] and the instance of [t] *) val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t +val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t + (* It may be handy to inject a simple term into the first form of cpattern *) val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern |