Define a minimal subset of Module(Type) Declarations in template-coq - #739

Draft

yeejian-tan wants to merge 50 commits into

MetaRocq:coq-8.16from

yeejian-tan:global-env-tree

Commits on Jun 14, 2022

Update docker image version.
mattam82
committed
511bcda
Merge pull request #712 from MetaCoq/fix-8.14-ci
mattam82
authored
f5e6231
Remove mutual inductiveness from whne def (#711)
arthur-adjedj
authored
1610c2d

Commits on Jun 17, 2022

Fill one admitted proof in Firstorder, remove dead code
mattam82
committed
74b9db2
Merge pull request #715 from MetaCoq/clean-admits-8.14
mattam82
authored
ffd483d

Commits on Jun 25, 2022

Option to see constructors as block in EWcbvEval, needed for extraction in CertiCoq and to OCaml/Malfunction (#716)
yforster
authored
63906fb

Commits on Jul 1, 2022

Replace all uses of `todo` and `Admitted` by axioms (#717)

yforster
and
mattam82
committed
488ac9d
Ensure constant constructors are declared in evaluation (#718)
mattam82
committed
b6daf8c
Update readmes (#719)
mattam82
committed
17b9492
Fix README
mattam82
committed
a247fa6
Remove warnings (#720)

yforster
authored and
mattam82
committed
f8510b0
Constructor tactic example (#725)
mattam82
committed
78b5df8
Constructors as blocks (#723)

mattam82
and
yforster
committed
5b410f1
[doc] Update erasure README.md for constructors-as-blocks
mattam82
committed
1f45662
Update README.md and self_erasure file
mattam82
committed
7fde2fb
Update DOC.md and dependency graph
mattam82
committed
0102668
Point to 8.14 branch in README
mattam82
committed
d921719
Revert "Option to see constructors as block in EWcbvEval, needed for extraction in CertiCoq and to OCaml/Malfunction (#716)"
mattam82
committed
58a3f1f
Fixes after merge
mattam82
committed
c97d948
Merge pull request #727 from MetaCoq/merge-8.16-in-8.14
mattam82
authored
5d2f136

Commits on Jul 5, 2022

Release changes 8.14 (#732)

mattam82
and
yforster
authored
c1dae3e

Commits on Jul 6, 2022

add support for nix, like #705 but as branch in this repo (#706)

yforster
and
kyoDralliam
authored
c6426d9

Commits on Jul 8, 2022

Ewellformed islambda (#735)
mattam82
authored
314186f

Commits on Jul 12, 2022

Constructors as blocks in the erasure pipeline (#736)
mattam82
authored
2320bd1

Commits on Jul 13, 2022

Use efficient maps in eta-expansion phase (#738)
mattam82
authored
836ec66
Write fixpoint attempt for on_module_decl (failed)
Yee-Jian Tan
committed
a9eb6f6
Define on_module_decl
Yee-Jian Tan
committed
1e90089
Define on_module_decl with induction principle
Yee-Jian Tan
committed
2845a4c
Proves on_global_env_impl
Yee-Jian Tan
committed
edd35a6
Done EnvironmentTyping, needs cleanup
Yee-Jian Tan
committed
82f2002
Proves theorem in Typing.v
Yee-Jian Tan
committed
d3bba3b
Defined check_wf_mod_body and friends
Yee-Jian Tan
committed
05aa36f
Cleanup todos and prove wf and eta properties
Yee-Jian Tan
committed
e490ade

Commits on Jul 14, 2022

Move to prop Qed'ed lemmas in type for cleaner extraction
mattam82
committed
8e2c7a4

Commits on Jul 18, 2022

Merge remote-tracking branch 'origin/coq-8.14' into global-env-tree
Yee-Jian Tan
committed
25646ca

Commits on Jul 19, 2022

Finish proving EtaExpand.v and remove Prints
Yee-Jian Tan
committed
3a0f226

Commits on Jul 20, 2022

Extend print_env for module (type) declarations
Yee-Jian Tan
committed
e1101bf

Commits on Dec 1, 2022

Before updating to coq-8.16
Yee-Jian Tan
committed
be8b6e9
fixup this
Yee-Jian Tan
committed
2ee944e
Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Yee-Jian Tan
committed
a5fd721

Commits on Dec 3, 2022

Fix some proofs
Yee-Jian Tan
committed
ab86056
More fixes
Yee-Jian Tan
committed
53afd12
Don't know how to derive reflection??
Yee-Jian Tan
committed
e11975f

Commits on Dec 7, 2022

Refactor structure_field and prove ReflectAst.v
Yee-Jian Tan
committed
8bbde7e
Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Yee-Jian Tan
committed
b4b4efa

Commits on Dec 23, 2022

Merge remote-tracking branch 'origin/coq-8.16' into global-env-tree
Yee-Jian Tan
committed
3887bfb
Create no-module environment for pcuic
Yee-Jian Tan
committed
e6974c5

Commits on Jan 15, 2023

TemplateToPcuic translation for modules
Yee-Jian Tan
committed
4c62462

Commits on Jan 17, 2023

nested inductive types
Yee-Jian Tan
committed
89b4c00

Commits on Feb 2, 2023

Define well-founded recursion on structure_field
Yee-Jian Tan
committed
58ce481