Commit 5be825cc authored by charguer's avatar charguer

export script

parent d5d1e6ea
# ---DEPRECATED---
# V_AUX := $(CFML)/lib/coq/Shared.v
# -R $(CFML)/lib/coq CFML \
# in export: cp -r $CFML/lib/coq/Shared.v $ARCHIVE/model/
\ No newline at end of file
......@@ -24,12 +24,11 @@ OTHER :=\
ModelTactics
PWD := $(shell pwd)
V_AUX := $(CFML)/lib/coq/Shared.v
V := $(addprefix $(PWD)/,$(SRC:=.v))
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R $(PWD) MODEL
include $(TLC)/Makefile.coq
......@@ -40,3 +39,4 @@ include $(TLC)/Makefile.coq
export:
./export.sh
scp -p -B -C seplogics.tar.gz yquem.inria.fr:public_html/dev/seplogics/
(*
(**
This file formalizes characteristic formulae for
......@@ -869,8 +871,4 @@ End CFWithLifting.
*)
\ No newline at end of file
(*
(**
This file formalizes characteristic formulae for
......@@ -492,8 +494,7 @@ Proof using. intros. applys* cf_sound. Qed.
*)
......
......@@ -261,11 +261,12 @@ Lemma state_disjoint_new : forall null (h:state) v,
Proof using.
intros null (m&(L&M)) v HF.
unfold state_disjoint, pfun_disjoint. simpl.
lets (l&F): (HF L).
lets (l&F): (HF (null::L)).
exists l. split.
{ intros l'. case_if~.
{ right. applys not_not_elim. intros H. applys F. applys~ M. } }
{ admit. (* TODO *) }
{ right. applys not_not_elim. intros H. applys F.
constructor. applys~ M. } }
{ intro_subst. applys~ F. }
Qed.
Lemma state_disjoint_single_set : forall (h:state) l v1 v2,
......
......@@ -30,8 +30,13 @@ cp $TLC/{*.v,Makefile,Makefile.coq} $ARCHIVE/TLC
# Copy a subset of CFML into the archive.
echo "Copying CFML/model..."
mkdir $ARCHIVE/model
cp -r $CFML/lib/coq/Shared.v $ARCHIVE/model/
cp -r $CFML/model/*.v $ARCHIVE/model/
cp $CFML/model/ModelState.v $ARCHIVE/model/
cp $CFML/model/ModelLambda.v $ARCHIVE/model/
cp $CFML/model/ModelSepFunctor.v $ARCHIVE/model/
cp $CFML/model/ModelSepBasic.v $ARCHIVE/model/
cp $CFML/model/ModelSepCredits.v $ARCHIVE/model/
cp $CFML/model/ModelSepRO.v $ARCHIVE/model/
(cd $CFML && $HASH) > $ARCHIVE/model/HASH
# Copy Makefile.model into the archive as model/Makefile.
......
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