diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 09:52:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-28 09:52:18 +0100 |
| commit | 5a540c372648493575461a298e04b9fa716661ad (patch) | |
| tree | a5c6a9b455b93841dc0960b8b0c1e78865c96b1a /plugins | |
| parent | ac006d8c87a7e921ed5a106aeba264bd6c8caa6c (diff) | |
| parent | 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (diff) | |
Merge PR #6248: [api] Remove aliases of `Evar.t`
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 83b454769..047ca509b 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -565,7 +565,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = if evlist = [] then 0, c0 else let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") - (fun (k,_) -> str(Evd.string_of_existential k)) evlist)); + (fun (k,_) -> Evar.print k) evlist)); let evplist = let depev = List.fold_left (fun evs (_,(_,t,_)) -> let t = EConstr.of_constr t in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 276b7c8ab..e63a05b78 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -396,7 +396,7 @@ let inv_dir = function L2R -> R2L | R2L -> L2R type pattern_class = | KpatFixed | KpatConst - | KpatEvar of existential_key + | KpatEvar of Evar.t | KpatLet | KpatLam | KpatRigid |