diff options
| author | Hugo Herbelin | 2020-08-13 16:54:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-13 16:54:17 +0200 |
| commit | ae5f5ba7f7e673dfeb06a9feaa4271fc165d01f3 (patch) | |
| tree | 9ef80c3a604814bb9f843f916b31b8e1220f9ecb /proofs | |
| parent | 2dbeadd72658eaa09cc9a683656aa27a4f140d50 (diff) | |
| parent | 404314c00175fcd67468bc0875c697d1c88d4650 (diff) | |
Merge PR #12720: Factor code related to class hint clenv
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 10 | ||||
| -rw-r--r-- | proofs/clenv.mli | 3 |
2 files changed, 0 insertions, 13 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9bd7ccda5d..db76d08736 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp -let refresh_undefined_univs clenv = - match EConstr.kind clenv.evd clenv.templval.rebus with - | Var _ -> clenv, Univ.empty_level_subst - | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst - | _ -> - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in - { clenv with evd = evd'; templval = map_freelisted clenv.templval; - templtyp = map_freelisted clenv.templtyp }, subst - let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c diff --git a/proofs/clenv.mli b/proofs/clenv.mli index fd1e2fe593..43e808dac7 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -45,9 +45,6 @@ val mk_clenv_from_n : Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv -(** Refresh the universes in a clenv *) -val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst - (** {6 linking of clenvs } *) val clenv_fchain : |