diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index ab4f3af79..35bed8f40 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -23,6 +23,9 @@ type clausenv = { out *) templtyp : constr freelisted (** its type *)} + +val map_clenv : (constr -> constr) -> clausenv -> clausenv + (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr @@ -41,6 +44,9 @@ val mk_clenv_from_n : val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv +(** Refresh the universes in a clenv *) +val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst + (** {6 linking of clenvs } *) val connect_clenv : Goal.goal sigma -> clausenv -> clausenv |