Generalization of the env8
Showing
- Makefile.coq.local 2 additions, 0 deletionsMakefile.coq.local
- README.md 1 addition, 0 deletionsREADME.md
- common-c-code/common_flight_plan.c 5 additions, 1 deletioncommon-c-code/common_flight_plan.c
- frontend/camlcoq_vfpg.ml 4 additions, 7 deletionsfrontend/camlcoq_vfpg.ml
- frontend/preproc.ml 1 addition, 3 deletionsfrontend/preproc.ml
- frontend/printer.ml 2 additions, 2 deletionsfrontend/printer.ml
- generated/CommonFP.v 9 additions, 4 deletionsgenerated/CommonFP.v
- src/common/CommonLemmasNat8.v 17 additions, 2 deletionssrc/common/CommonLemmasNat8.v
- src/generator/AuxFunctions.v 2 additions, 2 deletionssrc/generator/AuxFunctions.v
- src/generator/FBDerouteAnalysis.v 5 additions, 2 deletionssrc/generator/FBDerouteAnalysis.v
- src/generator/FPExtended.v 32 additions, 25 deletionssrc/generator/FPExtended.v
- src/generator/FPSizeVerification.v 155 additions, 67 deletionssrc/generator/FPSizeVerification.v
- src/generator/Generator.v 7 additions, 7 deletionssrc/generator/Generator.v
- src/semantics/FPBigStep.v 8 additions, 3 deletionssrc/semantics/FPBigStep.v
- src/semantics/FPBigStepClight.v 1 addition, 1 deletionsrc/semantics/FPBigStepClight.v
- src/semantics/FPBigStepExtended.v 59 additions, 6 deletionssrc/semantics/FPBigStepExtended.v
- src/semantics/FPBigStepGeneric.v 1 addition, 3 deletionssrc/semantics/FPBigStepGeneric.v
- src/semantics/FPBigStepSized.v 225 additions, 186 deletionssrc/semantics/FPBigStepSized.v
- src/semantics/FPEnvironment.v 11 additions, 1 deletionsrc/semantics/FPEnvironment.v
- src/semantics/FPEnvironmentExtended.v 20 additions, 3 deletionssrc/semantics/FPEnvironmentExtended.v
Please register or sign in to comment