diff options
| author | coqbot-app[bot] | 2020-12-10 17:23:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-10 17:23:32 +0000 |
| commit | 71031ef2a7032bccb55cc0e6035900c5b843583c (patch) | |
| tree | 3e568d98c1ccea2e2e5c9ab055c2163d9291db72 /pretyping/inductiveops.ml | |
| parent | c3ba8edf47e9afd1d2d226c2d006bbc7830b254a (diff) | |
| parent | dc7a4f056d97c43badaa6ca5901eafb951527d88 (diff) | |
Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanup of constrintern.ml
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23145b1629..bd875cf68b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) = let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] +let inductive_alltags env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags mip.mind_arity_ctxt + +let constructor_alltags env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1)) + let constructor_has_local_defs env (indsp,j) = let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in |