README

This code is an uptated versión of the original code found on this course which runs on Coq version 8.2pl2.
The actual versión of the code is Coq version 8.14.1
The coq files are the .v ones. The other ones are the compilations of the .v files, if you have coq v.8.14.1 you can actually just download it and run the code. If not, you would have to take the .v files and compile them one by one.

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
#Imp.v#		#Imp.v#
.Compil.aux		.Compil.aux
.Compil_smallstep.aux		.Compil_smallstep.aux
.Deadcode.aux		.Deadcode.aux
.Imp.aux		.Imp.aux
.Regalloc.aux		.Regalloc.aux
.Semantics.aux		.Semantics.aux
.Sequences.aux		.Sequences.aux
.SfLib.aux		.SfLib.aux
.lia.cache		.lia.cache
Compil.glob		Compil.glob
Compil.v		Compil.v
Compil.vo		Compil.vo
Compil.vok		Compil.vok
Compil.vos		Compil.vos
Compil_smallstep.glob		Compil_smallstep.glob
Compil_smallstep.v		Compil_smallstep.v
Compil_smallstep.vo		Compil_smallstep.vo
Compil_smallstep.vok		Compil_smallstep.vok
Compil_smallstep.vos		Compil_smallstep.vos
Deadcode.glob		Deadcode.glob
Deadcode.v		Deadcode.v
Deadcode.vo		Deadcode.vo
Deadcode.vok		Deadcode.vok
Deadcode.vos		Deadcode.vos
Imp.glob		Imp.glob
Imp.v		Imp.v
Imp.vo		Imp.vo
Imp.vok		Imp.vok
Imp.vos		Imp.vos
README.md		README.md
Regalloc.glob		Regalloc.glob
Regalloc.v		Regalloc.v
Regalloc.vo		Regalloc.vo
Regalloc.vok		Regalloc.vok
Regalloc.vos		Regalloc.vos
Semantics.glob		Semantics.glob
Semantics.v		Semantics.v
Semantics.vo		Semantics.vo
Semantics.vok		Semantics.vok
Semantics.vos		Semantics.vos
Sequences.glob		Sequences.glob
Sequences.v		Sequences.v
Sequences.vo		Sequences.vo
Sequences.vok		Sequences.vok
Sequences.vos		Sequences.vos
SfLib.glob		SfLib.glob
SfLib.v		SfLib.v
SfLib.vo		SfLib.vo
SfLib.vok		SfLib.vok
SfLib.vos		SfLib.vos
_CoqProject		_CoqProject
thesis.pdf		thesis.pdf

Provide feedback