Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

SProp #708

Draft
wants to merge 17 commits into
base: coq-8.14
Choose a base branch
from
Draft

SProp #708

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
edb57ee
Rebase relevance Template
yannl35133 May 4, 2022
ba7ef6c
Rebase relevance pcuic
yannl35133 May 5, 2022
09d673a
First files of safechecker
yannl35133 May 6, 2022
e7e08f8
Relevance on terms
yannl35133 May 4, 2022
6bacff9
Compatibility between relevance from syntax and relevance from type
yannl35133 May 17, 2022
120be9d
Factor out admissions, safechecker
yannl35133 May 19, 2022
a6d7c5f
Erasure
yannl35133 May 20, 2022
477ea5d
Add the missing file to PluginProject
yannl35133 May 23, 2022
eeb7014
Add wf hypothesis to admitted lemmas
yannl35133 May 23, 2022
761890a
Make isTermRel an inductive predicate
yannl35133 May 24, 2022
dfaf094
Plugin fix
yannl35133 May 24, 2022
4c38291
Fill the auxilliary lemmas about the relevance of constructors/induct…
mattam82 May 24, 2022
5162310
Fill the proof for projections as well
mattam82 May 25, 2022
ea6493a
Adapt to new projection_type(_and_eq) lemmas
mattam82 May 25, 2022
35cd102
Move lemmas to their right place
mattam82 May 26, 2022
c2699f9
Replace typ_or_sort with a judgment type (binary or ternary with opti…
yannl35133 Jun 10, 2022
6adeff3
Prepare for rebase
yannl35133 Jul 5, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions erasure/_PluginProject.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,8 +106,6 @@ src/eInduction.ml
src/eInduction.mli
src/eEtaExpanded.mli
src/eEtaExpanded.ml
# src/eInduction.ml
# src/eInduction.mli
src/eLiftSubst.ml
src/eLiftSubst.mli
src/eCSubst.mli
Expand Down
13 changes: 0 additions & 13 deletions erasure/src/metacoq_erasure_plugin.mlpack
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,30 +1,18 @@
MSetWeakList
EqdepFacts
Ssrbool
Ssreflect
Utils

WGraph
UGraph0
EnvMap

WcbvEval
Classes0
Logic1
Relation
Relation_Properties
PCUICAst
PCUICCases
PCUICAstUtils
EqDecInstances
PCUICEquality
PCUICTyping
PCUICInduction
PCUICWfUniverses
PCUICNormal
PCUICPosition
PCUICPretty
PCUICWcbvEval
PCUICProgram
TemplateToPCUIC
PCUICExpandLets
Expand All @@ -34,7 +22,6 @@ PCUICErrors
PCUICEqualityDec
PCUICWfEnv
PCUICWfEnvImpl
PCUICUnivSubst
PCUICSafeReduce
PCUICSafeRetyping

Expand Down
Loading