Code

PCUIC PHOAS#573

Code

Open

mattam82 wants to merge 147 commits intocoq-8.14MetaRocq/metarocq:coq-8.14from

pcuic-phoasMetaRocq/metarocq:pcuic-phoasCopy head branch name to clipboard

Commits

Commits on Oct 22, 2021

• Adapt to removal of first argument of PrivatePolymorphic in Coq #14727.

  herbelin

  committed
  dc339ff

  Copy full SHA for dc339ff

• Simplification of PrivatePolymorphism solves the coq/coq#14903 issue.

  Show description for ea3719f
  herbelin

  committed
  ea3719f

  Copy full SHA for ea3719f

Commits on Nov 25, 2021

• Fix reify/quote of predicate and branches binding name contexts (wrong order)

  mattam82

  committed
  75127a6

  Copy full SHA for 75127a6

Commits on Dec 11, 2021

• Adapt to coq/coq#15294 (comparison is no longer extracted to int)

  Lysxia

  committed
  129475b

  Copy full SHA for 129475b

Commits on Dec 14, 2021

• Merge pull request #621 from Lysxia/overlay-15294

  Show description for f309b9e
  TheoWinterhalter

  authored
  f309b9e

  Copy full SHA for f309b9e

Commits on Jan 4, 2022

• adapt to #14137

  Alizter

  committed
  cfa9984

  Copy full SHA for cfa9984

Commits on Jan 7, 2022

• adapt to coq/coq#15446

  olaure01

  committed
  d601c2f

  Copy full SHA for d601c2f

• Merge pull request #624 from Alizter/setoid-rewrite-type

  Show description for 35df3d3
  ppedrot

  authored
  35df3d3

  Copy full SHA for 35df3d3

Commits on Jan 10, 2022

• Merge pull request #628 from olaure01/signatureT

  Show description for 717d48c
  mattam82

  authored
  717d48c

  Copy full SHA for 717d48c

Commits on Jan 11, 2022

• Adapt w.r.t. coq/coq#15442.

  ppedrot

  committed
  bf8375e

  Copy full SHA for bf8375e

• Merge pull request #630 from ppedrot/deprecate-program-naming-mode

  Show description for edf5061
  ppedrot

  authored
  edf5061

  Copy full SHA for edf5061

Commits on Jan 12, 2022

• Missing adaptation to coq/coq#15442.

  ppedrot

  committed
  1368aec

  Copy full SHA for 1368aec

• Merge pull request #631 from ppedrot/deprecate-program-naming-mode-missing

  Show description for a44a2fd
  ppedrot

  authored
  a44a2fd

  Copy full SHA for a44a2fd

Commits on Jan 25, 2022

• Merge branch 'coq-8.14'

  mattam82

  committed
  06457c0

  Copy full SHA for 06457c0

Commits on Jan 26, 2022

• Fixes after merge

  mattam82

  committed
  bdaec46

  Copy full SHA for bdaec46

Commits on Jan 27, 2022

• Try to make the safechecker run again

  mattam82

  committed
  b19ebf8

  Copy full SHA for b19ebf8

• Make master compile some examples: universes are broken right now

  mattam82

  committed
  cc26139

  Copy full SHA for cc26139

• Finish updating master with 8.14 changes

  mattam82

  committed
  fc3a268

  Copy full SHA for fc3a268

• Fix Extraction files requiring Ascii

  mattam82

  committed
  7bebcd6

  Copy full SHA for 7bebcd6

Commits on Jan 28, 2022

• Fix build.yml to require coq.dev

  mattam82

  committed
  8f40d07

  Copy full SHA for 8f40d07

• Upate opam dependencies

  mattam82

  committed
  be3af83

  Copy full SHA for be3af83

• Call Coq's CList.filter_map

  mattam82

  committed
  176add0

  Copy full SHA for 176add0

• Move filter_map to tm_util

  mattam82

  committed
  eb780f4

  Copy full SHA for eb780f4

• Merge pull request #635 from MetaCoq/master-merge-8.14

  Show description for 0ee5bc8
  mattam82

  authored
  0ee5bc8

  Copy full SHA for 0ee5bc8

• pass on pcuic syntax

  MevenBertrand

  committed
  a149fee

  Copy full SHA for a149fee

• cleaning up the removal of ContextRelations

  MevenBertrand

  committed
  51b62f5

  Copy full SHA for 51b62f5

• document Nicolas' refactoring

  MevenBertrand

  committed
  21a0144

  Copy full SHA for 21a0144

• finished pass on pcuic

  MevenBertrand

  committed
  430252b

  Copy full SHA for 430252b

• pass on safechecker

  MevenBertrand

  committed
  09d855e

  Copy full SHA for 09d855e

• first batch of remarks by Théo

  MevenBertrand

  committed
  f495006

  Copy full SHA for f495006

• qualifying import to pass opam build

  MevenBertrand

  committed
  393a5b7

  Copy full SHA for 393a5b7

• removing useless notation

  MevenBertrand

  committed
  1413c65

  Copy full SHA for 1413c65

• Merge pull request #625 from MetaCoq/filesdoc

  Show description for cd3bc92
  MevenBertrand

  authored
  cd3bc92

  Copy full SHA for cd3bc92

Commits on Feb 1, 2022

• adapt to coq/coq#15220

  gares

  committed
  51ac3cb

  Copy full SHA for 51ac3cb

Commits on Feb 3, 2022

• Merge pull request #613 from gares/dynlink-w-findlib

  Show description for ec96734
  ppedrot

  authored
  ec96734

  Copy full SHA for ec96734

Commits on Feb 8, 2022

• Fix compilation of safechecker with findlib

  gares

  committed
  c69085d

  Copy full SHA for c69085d

• export OCAMLPATH

  gares

  committed
  7ffff46

  Copy full SHA for 7ffff46

• Avoid warning keeping template-coq/build around

  gares

  committed
  4026e06

  Copy full SHA for 4026e06

Commits on Feb 10, 2022

• META: safechecker depends on template

  gares

  committed
  0b893e2

  Copy full SHA for 0b893e2

• Merge pull request #640 from gares/fix-findlib

  Show description for 1e24c40
  mattam82

  authored
  1e24c40

  Copy full SHA for 1e24c40

• Change the univ representation so that global universes are really represented as a global context set

  mattam82

  committed
  96f5dee

  Copy full SHA for 96f5dee

• New global_env structure in template-coq/reification

  mattam82

  committed
  6b9e43b

  Copy full SHA for 6b9e43b

• Adapt PCUIC to new global_env structure

  mattam82

  committed
  cdb0762

  Copy full SHA for cdb0762

• Adapt Template -> PCUIC Correctness proof

  mattam82

  committed
  e406d57

  Copy full SHA for e406d57

• Fix udecl definition (was not including set in global levels)

  mattam82

  committed
  42d6c2b

  Copy full SHA for 42d6c2b

• Adapted safe_checker to new global env

  mattam82

  committed
  56fc551

  Copy full SHA for 56fc551

• Adapt erasure to new global env

  mattam82

  committed
  caa1b86

  Copy full SHA for caa1b86

• Adapted erasure to new environment representation

  mattam82

  committed
  b182531

  Copy full SHA for b182531

• Fix quoting

  mattam82

  committed
  ccc5499

  Copy full SHA for ccc5499

• Disable quoting of the universe graph for now

  mattam82

  committed
  bff9cc4

  Copy full SHA for bff9cc4

• Fix warnings in extraction, using `Stdlib` instead of `Pervasives`

  mattam82

  committed
  95387c7

  Copy full SHA for 95387c7

• Factorize Extraction files

  mattam82

  committed
  9209af0

  Copy full SHA for 9209af0

• Fix quoting of universe contexts/safecheck to use restricted graph

  mattam82

  committed
  1ad0f14

  Copy full SHA for 1ad0f14

• Adapt test-suite to change in global_env

  mattam82

  committed
  4a153c0

  Copy full SHA for 4a153c0

• Remove deprecation and other warnings

  mattam82

  committed
  9e99741

  Copy full SHA for 9e99741

• Try to fix weird type equality issue in ocaml 4.07.1

  mattam82

  committed
  085c7c6

  Copy full SHA for 085c7c6

• Minor fixes

  mattam82

  committed
  07776b1

  Copy full SHA for 07776b1

• Guard .merlin target: only applies when extracted files have been produced

  mattam82

  committed
  578f1c1

  Copy full SHA for 578f1c1

Commits on Feb 11, 2022

• Fix configure script call

  mattam82

  committed
  ff3336b

  Copy full SHA for ff3336b

• Fix template-coq Makefile requirerments for install target

  mattam82

  committed
  8ee8f75

  Copy full SHA for 8ee8f75

• Fix opam/findlib installation

  mattam82

  committed
  98bf5c2

  Copy full SHA for 98bf5c2

• Fix safechecker

  mattam82

  committed
  afc6d36

  Copy full SHA for afc6d36

• Fix local builds of plugins

  mattam82

  committed
  ebb430d

  Copy full SHA for ebb430d

• Make the local build not interfer with the global one

  mattam82

  committed
  5113744

  Copy full SHA for 5113744

• No more -I ../template_coq needed

  mattam82

  committed
  ed72148

  Copy full SHA for ed72148

• Make META a phony rule so it is properly regenerated for each plugni

  mattam82

  committed
  f64d8ca

  Copy full SHA for f64d8ca

• Remove _build directory, no longer needed

  mattam82

  committed
  fb0a5a8

  Copy full SHA for fb0a5a8

• Fix the test-suite makefiles

  mattam82

  committed
  15cc7dc

  Copy full SHA for 15cc7dc

• Fix examples Makefile

  mattam82

  committed
  e9f2ee2

  Copy full SHA for e9f2ee2

• No longer mkdir build

  mattam82

  committed
  2598ee4

  Copy full SHA for 2598ee4

• Fix translations

  mattam82

  committed
  2c38bc1

  Copy full SHA for 2c38bc1

• Merge pull request #634 from MetaCoq/master-global-universes

  Show description for b5e4809
  mattam82

  authored
  b5e4809

  Copy full SHA for b5e4809

• Update copyright notice in README

  mattam82

  authored
  b077764

  Copy full SHA for b077764

Commits on Feb 14, 2022

• Merge pull request #599 from herbelin/master+adapt-coq-pr14727-reworking-cooking

  Show description for 8531d62
  ppedrot

  authored
  8531d62

  Copy full SHA for 8531d62

Commits on Feb 16, 2022

• Add stdlib-shims dependency to compile with ocaml < 4.07

  mattam82

  committed
  42fb30a

  Copy full SHA for 42fb30a

• Merge pull request #647 from MetaCoq/stdlib-shims-dep

  Show description for 5962851
  mattam82

  authored
  5962851

  Copy full SHA for 5962851

• Update the META files for the dependency on stdlib-shims as well

  mattam82

  committed
  af51a04

  Copy full SHA for af51a04

Commits on Feb 17, 2022

• Merge branch 'coq-8.14' into master-merge-8.14

  mattam82

  committed
  b638bfe

  Copy full SHA for b638bfe

• Fix a typo

  mattam82

  committed
  321f34d

  Copy full SHA for 321f34d

• Revert extraction of nat to int (not compatible with certicoq)

  mattam82

  committed
  f09c0db

  Copy full SHA for f09c0db

• Merge pull request #648 from MetaCoq/master-merge-8.14

  Show description for 804d9ee
  mattam82

  authored
  804d9ee

  Copy full SHA for 804d9ee

Commits on Mar 16, 2022

• Adapt to coq/coq#15754 (#655)

  proux01

  authored
  234a829

  Copy full SHA for 234a829

Commits on Mar 21, 2022

• Adapt w.r.t. coq/coq#15837.

  ppedrot

  committed
  f0a3a56

  Copy full SHA for f0a3a56

Commits on Mar 22, 2022

• Merge pull request #668 from ppedrot/reduce-universe-footprint

  Show description for 9793d93
  ppedrot

  authored
  9793d93

  Copy full SHA for 9793d93

Commits on Mar 25, 2022

• Adapt w.r.t. coq/coq#15856.

  ppedrot

  committed
  4845d2a

  Copy full SHA for 4845d2a

Commits on Mar 28, 2022

• Merge pull request #670 from ppedrot/universes-rm-univ-of-sort

  Show description for 72667aa
  ppedrot

  authored
  72667aa

  Copy full SHA for 72667aa

Commits on Mar 29, 2022

• Adapt w.r.t. coq/coq#15863.

  ppedrot

  committed
  1cf25d9

  Copy full SHA for 1cf25d9

• Merge pull request #673 from ppedrot/universes-rm-small-levels

  Show description for 90dbbcb
  ppedrot

  authored
  90dbbcb

  Copy full SHA for 90dbbcb

Commits on Mar 30, 2022

• Adapt w.r.t. coq/coq#15871.

  ppedrot

  committed
  0914586

  Copy full SHA for 0914586

Commits on Mar 31, 2022

• Merge pull request #674 from ppedrot/univ-cleanup-api

  Show description for d012c81
  ppedrot

  authored
  d012c81

  Copy full SHA for d012c81

Commits on Apr 25, 2022

• Merge pull request #649 from MetaCoq/extraction-no-ascii

  Show description for 374086a
  mattam82

  committed
  374086a

  Copy full SHA for 374086a

• Merge pull request #652 from MetaCoq/remove-primitives

  Show description for 7478e56
  mattam82

  committed
  7478e56

  Copy full SHA for 7478e56

• Merge pull request #653 from MetaCoq/self-erasure

  Show description for 38c93a4
  mattam82

  committed
  38c93a4

  Copy full SHA for 38c93a4

• Merge pull request #654 from MetaCoq/parameter-stripping

  Show description for e30240f
  mattam82

  committed
  e30240f

  Copy full SHA for e30240f

• Parameter stripping integration (#656)

  Show description for fa458d8
  mattam82

  committed
  fa458d8

  Copy full SHA for fa458d8

• Generic EnvMap (#658)

  Show description for 8af7ac2
  mattam82

  committed
  8af7ac2

  Copy full SHA for 8af7ac2

• Clean erasure (#661)

  Show description for 83b4f94
  mattam82

  committed
  83b4f94

  Copy full SHA for 83b4f94

• Abstract env for safetyping (#662)

  Show description for 7bdd877
  

  tabareau

  authored and

  mattam82

  committed
  7bdd877

  Copy full SHA for 7bdd877

• Merge pull request #663 from MetaCoq/bytestring

  Show description for 9a18b38
  mattam82

  committed
  9a18b38

  Copy full SHA for 9a18b38

• Merge pull request #664 from kyoDralliam/fix-case-insensitive

  Show description for a75750c
  mattam82

  committed
  a75750c

  Copy full SHA for a75750c

• Merge pull request #665 from kyoDralliam/fix-file-ambiguity

  Show description for 20f630e
  mattam82

  committed
  20f630e

  Copy full SHA for 20f630e

• Merge pull request #667 from MetaCoq/hnf_ctor_types

  Show description for 9c66c7b
  mattam82

  committed
  9c66c7b

  Copy full SHA for 9c66c7b

• Add a relevance field to constant bodies (#666)

  Show description for 272c438
  mattam82

  committed
  272c438

  Copy full SHA for 272c438

• Implement a `infer_univs` mode for mkInductive (#612)

  Show description for 4058bc6
  mattam82

  committed
  4058bc6

  Copy full SHA for 4058bc6

• Abstract env check (#671)

  Show description for 9169639
  

  tabareau

  authored and

  mattam82

  committed
  9169639

  Copy full SHA for 9169639

• Eta expand fixpoints (#669)

  Show description for 00a137a
  mattam82

  committed
  00a137a

  Copy full SHA for 00a137a

• Merge pull request #675 from MetaCoq/typing-wf-forall-decls

  Show description for 73203c8
  

  tabareau

  authored and

  mattam82

  committed
  73203c8

  Copy full SHA for 73203c8

• Reorganise Universes.v and have check_univs only alter level [exprs] checks (#672)

  Show description for c2453fe
  

  yannl35133

  authored and

  mattam82

  committed
  c2453fe

  Copy full SHA for c2453fe

• Thread eta expansion everywhere (#676)

  Show description for 7790324
  mattam82

  committed
  7790324

  Copy full SHA for 7790324

• Update .gitignore

  mattam82

  committed
  0fcb5ba

  Copy full SHA for 0fcb5ba

• Missing links in PCUIC’s Readme

  Show description for 65f8e13
  

  MevenBertrand

  authored and

  mattam82

  committed
  65f8e13

  Copy full SHA for 65f8e13

• Erasure optimizations preserves wellformedness and expansion (#677)

  Show description for a5b3a05
  mattam82

  committed
  a5b3a05

  Copy full SHA for a5b3a05

• Merge pull request #678 from MetaCoq/eenvmap-in-optimize-prop-discr

  Show description for b63ce43
  mattam82

  committed
  b63ce43

  Copy full SHA for b63ce43

• Strict eta expanded constructors (#680)

  Show description for 2266b98
  mattam82

  committed
  2266b98

  Copy full SHA for 2266b98

• Refinements of EWellformed and EWcbvEvalEtaInd (#681)

  Show description for 5d66647
  mattam82

  committed
  5d66647

  Copy full SHA for 5d66647

• Inline projections optimization (#683)

  Show description for 1d6c6d3
  mattam82

  committed
  1d6c6d3

  Copy full SHA for 1d6c6d3

• Make safechecker compute (#682)

  Show description for 1495a1e
  

  tabareau

  authored and

  mattam82

  committed
  1495a1e

  Copy full SHA for 1495a1e

• Merge pull request #684 from MetaCoq/erasure-cleanups

  Show description for 9244ffb
  mattam82

  committed
  9244ffb

  Copy full SHA for 9244ffb

• Slightly faster erasure of global environments (#685)

  Show description for 3bbfbd9
  mattam82

  committed
  3bbfbd9

  Copy full SHA for 3bbfbd9

• Merge pull request #686 from MetaCoq/hott-tests

  Show description for ef9a873
  mattam82

  committed
  ef9a873

  Copy full SHA for ef9a873

• Use explicit records for projection names and declarations, add irrelevance (#689)

  Show description for 8d8f3bc
  mattam82

  committed
  8d8f3bc

  Copy full SHA for 8d8f3bc

• Remove accidentaly commited file

  Show description for 881d6df
  mattam82

  committed
  881d6df

  Copy full SHA for 881d6df

• Merge pull request #690 from MetaCoq/safeconversion-admit-free

  Show description for 9392e04
  mattam82

  committed
  9392e04

  Copy full SHA for 9392e04

• add constraints between monomorphic sorts to udecl (#687)

  Show description for 0daa598
  

  kyoDralliam

  authored and

  mattam82

  committed
  0daa598

  Copy full SHA for 0daa598

• Merge pull request #692 from MetaCoq/writing_cleanups

  Show description for acd3b3c
  mattam82

  committed
  acd3b3c

  Copy full SHA for acd3b3c

• Merge pull request #691 from MetaCoq/cleanup-all-erasure

  Show description for bb38e92
  mattam82

  committed
  bb38e92

  Copy full SHA for bb38e92

• Fixes after merge of 8.14 changes

  mattam82

  committed
  76ee01d

  Copy full SHA for 76ee01d

• Merge pull request #694 from MetaCoq/master-8.14-merge

  Show description for cbac790
  mattam82

  authored
  cbac790

  Copy full SHA for cbac790

Commits on Apr 27, 2022

• Adapt w.r.t. coq/coq#15943.

  ppedrot

  committed
  9474d7c

  Copy full SHA for 9474d7c

Commits on Apr 28, 2022

• Merge pull request #698 from ppedrot/cache-projection-relevance

  Show description for 42dba86
  ppedrot

  authored
  42dba86

  Copy full SHA for 42dba86

Commits on Jun 8, 2022

• Merge coq-8.14 branch in master

  mattam82

  committed
  c104fb3

  Copy full SHA for c104fb3

Commits on Jun 9, 2022

• Fixes after merge of 8.14 branch

  mattam82

  committed
  c35be57

  Copy full SHA for c35be57

• Fix build.yml

  mattam82

  committed
  8b835e7

  Copy full SHA for 8b835e7

• Fix `quick` target by setting universe checking in translation_utils.v

  mattam82

  committed
  7d16657

  Copy full SHA for 7d16657

• Fix generous_packed

  mattam82

  committed
  dc7848b

  Copy full SHA for dc7848b

Commits on Jun 15, 2022

• Update master status badge

  mattam82

  committed
  ea94a7f

  Copy full SHA for ea94a7f

• Fix CI instructions

  mattam82

  committed
  d98e388

  Copy full SHA for d98e388

• Fix CI instructions

  mattam82

  committed
  290e3b2

  Copy full SHA for 290e3b2

Commits on Jun 17, 2022

• Fill one admitted proof in Firstorder, remove dead code

  mattam82

  committed
  4461fe7

  Copy full SHA for 4461fe7

• Merge pull request #713 from MetaCoq/clean-admits

  Show description for 4c8b06d
  mattam82

  authored
  4c8b06d

  Copy full SHA for 4c8b06d

Commits on Jun 26, 2022

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

  Show description for daf3e47
  

  yforster

  and

  mattam82

  authored
  daf3e47

  Copy full SHA for daf3e47

Commits on Jun 27, 2022

• Ensure constant constructors are declared in evaluation (#718)

  mattam82

  authored
  29126ac

  Copy full SHA for 29126ac

• Update readmes (#719)

  Show description for ea2d0be
  mattam82

  authored
  ea2d0be

  Copy full SHA for ea2d0be

• Fix README

  mattam82

  committed
  8e541ec

  Copy full SHA for 8e541ec

Commits on Jun 28, 2022

• Remove warnings (#720)

  Show description for f6d8e17
  yforster

  authored
  f6d8e17

  Copy full SHA for f6d8e17

Commits on Jun 29, 2022

• Add a PCUICPHOAS file implementing a PHOAS variant of the syntax

  mattam82

  committed
  5a9c2aa

  Copy full SHA for 5a9c2aa

• Allow giving only one binder name and retriviing it in the phoas representation

  mattam82

  committed
  f03ae80

  Copy full SHA for f03ae80