Commit 2ac9d251 authored by charguer's avatar charguer

imports

parent 922bc91b
......@@ -8,8 +8,9 @@ License: MIT.
*)
Require Export LambdaSepLifted LambdaCFLifted.
Require Export LambdaStructLifted LibListZ.
From Sep Require Export LambdaSepLifted LambdaCFLifted.
From Sep Require Export LambdaStructLifted.
From TLC Require Export LibListZ.
Open Scope Z_scope.
(* Open Scope charac. TODO: not needed? *)
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import Example ExampleBasicNonlifted.
From Sep Require Import Example ExampleBasicNonlifted.
Generalizable Variables A B.
Implicit Type p q : loc.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LambdaSep LambdaCF TLCbuffer LambdaStruct.
From Sep Require Import LambdaSep LambdaCF TLCbuffer LambdaStruct.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import Example.
From Sep Require Import Example.
Generalizable Variables A B.
Implicit Types p : loc.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import Example.
From Sep Require Import Example.
Generalizable Variables A B.
Implicit Types p : loc.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LambdaCF LambdaStruct.
From Sep Require Import LambdaCF LambdaStruct.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
......
......@@ -9,7 +9,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import Example LibSet.
From Sep Require Import Example.
From TLC Require Import LibSet.
Generalizable Variables A B.
Implicit Types x : int.
......@@ -291,7 +292,7 @@ Qed.
(* ********************************************************************** *)
(* * Binary search trees *)
Require Import LibOrder.
From TLC Require Import LibOrder.
(* ---------------------------------------------------------------------- *)
(* ** Representation *)
......
......@@ -10,7 +10,7 @@ License: MIT.
Set Implicit Arguments.
Require Import LambdaCF LambdaStruct.
From Sep Require Import LambdaCF LambdaStruct.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
......@@ -22,7 +22,7 @@ Implicit Types n : int.
(* ********************************************************************** *)
(* * Union find *)
Require Import LibListZ.
From TLC Require Import LibListZ.
(* ---------------------------------------------------------------------- *)
(** Invariants *)
......
......@@ -11,7 +11,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LibCore.
From TLC Require Import LibCore.
(* ********************************************************************** *)
......
......@@ -9,7 +9,8 @@ License: MIT.
Set Implicit Arguments.
Require Export LibFix LambdaSep.
From TLC Require Export LibFix.
From Sep Require Export LambdaSep.
Open Scope heap_scope.
Implicit Types v w : val.
......
......@@ -11,7 +11,8 @@ License: MIT.
Set Implicit Arguments.
Require Export LibFix LambdaSepCredits. (* MODIFIED FOR CREDITS *)
From TLC Require Export LibFix.
From Sep Require Export LambdaSepCredits. (* MODIFIED FOR CREDITS *)
Open Scope heap_scope.
Implicit Types v w : val.
......
......@@ -11,7 +11,8 @@ License: MIT.
Set Implicit Arguments.
Require Export LibCore LambdaCF LambdaSepLifted.
From TLC Require Export LibCore.
From Sep Require Export LambdaCF LambdaSepLifted.
Generalizable Variables A B.
Open Scope charac.
......
......@@ -3048,7 +3048,7 @@ Fixpoint nat_fold A (f:nat->A->A) (k:nat) (z:A) : A :=
(** Recovering variable names in ltac *)
Require Import String.
Require Import Coq.Strings.String.
Open Scope string_scope.
Ltac with_var_name x cont :=
......
......@@ -12,7 +12,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LibCore Fmap TLCbuffer.
From TLC Require Export LibCore.
From Sep Require Export Fmap TLCbuffer.
(* ********************************************************************** *)
......
......@@ -16,7 +16,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LambdaSemantics SepTactics.
From Sep Require Export LambdaSemantics SepTactics.
Open Scope fmap_scope.
Ltac auto_star ::= jauto.
......
......@@ -24,7 +24,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LambdaSemantics SepTactics.
From Sep Require Export LambdaSemantics SepTactics.
Open Scope fmap_scope.
......
......@@ -14,7 +14,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LibCore LambdaSep.
From TLC Require Import LibCore.
From Sep Require Import LambdaSep.
Generalizable Variables A B.
Open Scope trm_scope.
......
......@@ -16,7 +16,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LambdaSemantics SepTactics.
From Sep Require Export LambdaSemantics SepTactics.
Open Scope fmap_scope.
Arguments exist [A] [P].
......@@ -1260,7 +1260,6 @@ Qed.
(* ********************************************************************** *)
(* * Extension: [normally] modality (WORK IN PROGRESS) *)
Module Normally.
Definition normally H :=
Hexists H1 H2, \[normal H1] \* H1 \* \[H1 \* RO H2 ==> H].
......
......@@ -9,8 +9,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require LibListZ.
Require Import LambdaCF TLCbuffer.
From TLC Require LibListZ.
From Sep Require Import LambdaCF TLCbuffer.
Open Scope trm_scope.
Open Scope heap_scope.
Open Scope charac.
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LambdaStruct LambdaCFLifted.
From Sep Require Export LambdaStruct LambdaCFLifted.
Open Scope trm_scope.
Open Scope charac.
Generalizable Variables A.
......
......@@ -6,17 +6,23 @@ CFML := ..
include $(CFML)/Makefile.common
# VERBOSE := 1
COQFLAGS:=-w -notation-overridden,-implicits-in-term
##############################################################################
# Compilation.
# The official list of files that should be compiled by [make]
# and included in the archive by [make export].
SRC := $(shell cat FILES)
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
ifeq ($(ARTHUR),1)
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
# The official list of files that should be compiled by [make]
# is stored in the file "FILES" and included in the archive by
# [make export].
#
ifeq ($(EXPORT),1)
SRC := $(shell cat FILES)
endif
PWD := $(shell pwd)
......@@ -25,7 +31,7 @@ V := $(addprefix $(PWD)/,$(SRC:=.v))
COQINCLUDE := \
-R $(TLC) TLC \
-R $(PWD) MODEL
-R $(PWD) Sep
include $(TLC)/Makefile.coq
......
......@@ -25,7 +25,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LibCore TLCbuffer.
From TLC Require Export LibCore.
From Sep Require Export TLCbuffer.
(* ********************************************************************** *)
......
......@@ -37,7 +37,8 @@ License: MIT.
*)
Set Implicit Arguments.
Require Export LibCore TLCbuffer SepFunctor.
From TLC Require Export LibCore.
From Sep Require Export TLCbuffer SepFunctor.
Module SepLogicTactics (SL : SepLogicCore).
......
......@@ -10,8 +10,8 @@ License: MIT.
Set Implicit Arguments.
Require Import LibTactics LibLogic LibList.
Require LibListZ.
From TLC Require Import LibTactics LibLogic LibList.
From TLC Require LibListZ.
Generalizable Variables A B.
......@@ -19,7 +19,7 @@ Generalizable Variables A B.
(*----------------------*)
(* Nat *)
Require Import LibNat LibInt.
From TLC Require Import LibNat LibInt.
Section NatSimpl.
......@@ -66,8 +66,8 @@ Hint Rewrite nat_zero_plus nat_plus_zero nat_plus_succ
(*----------------------*)
(* ListExec *)
Require Import LibLogic. (* needed? *)
Require Import LibReflect.
From TLC Require Import LibLogic. (* needed? *)
From TLC Require Import LibReflect.
(* TODO: LibListExec : is_not_nil *)
Definition is_not_nil A (l:list A) : bool :=
......
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