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
_PluginProject.in 
-I src
-R theories MetaCoq.Extraction

src/eAst.ml
src/eAst.mli
src/eAstUtils.ml
src/eAstUtils.mli
src/eInduction.ml
src/eInduction.mli
src/eLiftSubst.ml
src/eLiftSubst.mli
src/eTyping.ml
src/eTyping.mli
src/extract.mli
src/extract.ml
src/metacoq_extraction_plugin.mlpack
back to top