diff options
| author | Pierre-Marie Pédrot | 2019-03-15 17:33:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:01:05 +0100 |
| commit | 0d7365e6ddcbd14933fcedae777649d31fb311cc (patch) | |
| tree | 447738ad076030619ab8d1ab0f6273753449bf32 /engine/eConstr.mli | |
| parent | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (diff) | |
EConstr iterators respect the binding structure of cases.
Fixes #3166.
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 2add7b0b5e..e914d4f884 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -343,6 +343,10 @@ val is_global : Evd.evar_map -> GlobRef.t -> t -> bool val expand_case : Environ.env -> Evd.evar_map -> case -> (case_info * t * case_invert * t * t array) +val annotate_case : Environ.env -> Evd.evar_map -> case -> + case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array +(** Same as above, but doesn't turn contexts into binders *) + val expand_branch : Environ.env -> Evd.evar_map -> EInstance.t -> t array -> constructor -> case_branch -> rel_context (** Given a universe instance and parameters for the inductive type, |