diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /plugins/ssr/ssrcommon.mli | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'plugins/ssr/ssrcommon.mli')
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 2eadd5f26..c39945194 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -190,7 +190,7 @@ val pf_merge_uc_of : val constr_name : evar_map -> EConstr.t -> Name.t val pf_type_of : Goal.goal Evd.sigma -> - Term.constr -> Goal.goal Evd.sigma * Term.types + Constr.constr -> Goal.goal Evd.sigma * Constr.types val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types @@ -220,7 +220,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : Globnames.global_reference -> Goal.goal Evd.sigma -> - Term.constr * Goal.goal Evd.sigma + Constr.constr * Goal.goal Evd.sigma val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t @@ -232,7 +232,7 @@ val new_tmp_id : val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Goal.goal Evd.sigma -> - evar_map * Term.constr -> int * Term.constr + evar_map * Constr.constr -> int * Constr.constr val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int val gen_tmp_ids : ?ist:Geninterp.interp_sign -> |