diff options
| author | Pierre-Marie Pédrot | 2020-07-16 19:34:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | a666788182bce7059e6ba41b917b5ca6ab52ae13 (patch) | |
| tree | 00221510912864d8c6bb73c061b1a8478796f5bc /proofs | |
| parent | de16cf5411c2696044d5b17cccb3659d21a79921 (diff) | |
Code simplification around hint manipulation in Class_tactics.
We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
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 : |