Skip to main content

Browse the archive

Revision b955d35c81d840f502f359e8e29a81387a6f9385 authored by Théo Winterhalter on 06 July 2019, 20:42:59 UTC, committed by GitHub on 06 July 2019, 20:42:59 UTC 
Merge pull request #197 from yforster/new-erasure
 
Implementation of erasure
2 parent s 30ef5a5 + 22d6b3e
Raw File
_CoqProject.in 
-R theories MetaCoq.Extraction

theories/EAst.v
theories/EAstUtils.v
theories/EInduction.v
theories/ELiftSubst.v
theories/EWcbvEval.v
theories/EWndEval.v
theories/ETyping.v
theories/Extract.v
theories/EAll.v
theories/Extraction.v
theories/Prelim.v
theories/ESubstitution.v
theories/EInversion.v
theories/EArities.v
theories/ExtractionCorrectness.v
theories/ErasureFunction.v
back to top