Commit 23894085 authored by charguer's avatar charguer

renaming of model files

parent eb7871f7
ModelState
ModelLambda
ModelSepFunctor
ModelSepBasic
ModelSepCredits
ModelSepRO
ModelCF
ModelCFCredits
LibState
LambdaSemantics
SepFunctor
LambdaSep
LambdaSepCredits
LambdaSepRO
LambdaCF
LambdaCFCredits
\ No newline at end of file
......@@ -10,7 +10,7 @@ License: MIT.
Set Implicit Arguments.
Require Export LibFix ModelSepBasic.
Require Export LibFix LambdaSep.
Open Scope heap_scope.
......
......@@ -11,7 +11,7 @@ License: MIT.
Set Implicit Arguments.
Require Export LibFix ModelSepCredits. (* MODIFIED FOR CREDITS *)
Require Export LibFix LambdaSepCredits. (* MODIFIED FOR CREDITS *)
Open Scope heap_scope.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LibCore ModelSepML ModelCFML.
Require Import LibCore MLSep MLCF.
Open Scope trm_scope.
Open Scope heap_scope.
Open Scope charac.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LibCore ModelState.
Require Export LibCore LibState.
(************************************************************)
......
......@@ -5,7 +5,7 @@ Arthur Charguéraud's lecture notes.
This file contains:
- a definition of heaps as finite maps from location to values,
- an instantiation of the functor from the file ModelSepFunctor.v,
- an instantiation of the functor from the file SepFunctor.v,
- a definition of triples,
- statement and proofs of SL reasoning rules.
......@@ -15,7 +15,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export ModelLambda ModelSepFunctor.
Require Export LambdaSemantics SepFunctor.
Open Scope state_scope.
Ltac auto_star ::= jauto.
......
......@@ -14,7 +14,7 @@ François Pottier described in the following papers:
This file contains:
- a definition of heaps as finite maps from location to values
paired with a natural number,
- an instantiation of the functor from the file ModelSepFunctor.v,
- an instantiation of the functor from the file SepFunctor.v,
- a definition of triples,
- statement and proofs of SL reasoning rules.
......@@ -24,7 +24,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export ModelLambda ModelSepFunctor.
Require Export LambdaSemantics SepFunctor.
Open Scope state_scope.
......
......@@ -6,7 +6,7 @@ paper by Arthur Charguéraud and François Pottier.
This file contains:
- a definition of heaps as pairs of states,
- an instantiation of the functor from the file ModelSepFunctor.v,
- an instantiation of the functor from the file SepFunctor.v,
- a definition of triples,
- statement and proofs of SL reasoning rules.
......@@ -16,7 +16,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export ModelLambda ModelSepFunctor.
Require Export LambdaSemantics SepFunctor.
Open Scope state_scope.
Implicit Arguments exist [A P].
......
......@@ -12,7 +12,7 @@ License: MIT.
Set Implicit Arguments.
Require Export LibFix ModelSepML.
Require Export LibFix MLSep.
Open Scope heap_scope.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LibCore ModelState.
Require Export LibCore LibState.
(*------------------------------------------------------------------*)
......
......@@ -10,7 +10,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export ModelML ModelSepFunctor.
Require Export MLSemantics SepFunctor.
Open Scope state_scope.
Ltac auto_star ::= jauto.
......
This diff is collapsed.
......@@ -14,10 +14,10 @@ include $(CFML)/Makefile.common
# and included in the archive by [make export].
SRC := $(shell cat FILES)
SRC := ModelState ModelLambda ModelSepFunctor ModelSepBasic ModelSepCredits ModelSepRO ModelCF ModelCFCredits ModelML ModelSepML ModelCFML ModelSepExamples
ifeq ($(ARTHUR),1)
SRC = ModelState ModelSepFunctor ModelML ModelSepML ModelCFML ModelSepExamples
# LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits LambdaExamples
# LambdaExamples
SRC := LibState SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted
endif
PWD := $(shell pwd)
......
......@@ -38,7 +38,8 @@ mkdir $ARCHIVE/TLC
echo "Copying CFML/model..."
mkdir $ARCHIVE/model
if [ ! -z ${ARTHUR+x} ]; then
FILES="ModelState ModelLambda ModelSepFunctor ModelSepBasic ModelSepCredits ModelSepRO ModelCF ModelCFCredits ModelML ModelSepML ModelCFML ModelSepExamples"
FILES="LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits LambdaExamples MLSemantics MLSep MLSepLifted MLCF MLCFLifted"
# LambdaCFComplete
else
FILES=`grep -v -e "^ *#" FILES` ;
fi
......@@ -84,3 +85,5 @@ rm -rf $ARCHIVE
echo "Testing installation..."
make -C $ARCHIVE -j4
echo "OK."
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment