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/clenv.mli | |
| 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/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 : |