Why is there `extends_decls`

(rather than `extends`

) in

```
Definition Informative `{cf : checker_flags} (Σ : global_env_ext) (ind : inductive) :=
forall mdecl idecl,
declared_inductive (fst Σ) ind mdecl idecl ->
forall Γ args u n (Σ' : global_env_ext),
wf_ext Σ' ->
extends_decls Σ Σ' ->
Is_proof Σ' Γ (mkApps (tConstruct ind n u) args) ->
#|ind_ctors idecl| <= 1 /\
squash (All (Is_proof Σ' Γ) (skipn (ind_npars mdecl) args)).
```

?

I'm trying to figure out what the semantic content of this definition is, so that in my weakening of `extends`

to allow reordering, I can understand whether I'm supposed to be weakening or strengthening `extends_decls`

here (or, if it's important that it's exactly `extends_decls`

and not anything weaker nor stronger, I'd like to understand why that is).

I think it is extends_decls because that's what I needed in proofs. So consequently, it could probably anything else that still makes the proofs around erasure work

Last updated: Jun 04 2023 at 22:30 UTC