From 5dbddbde14875c1901fd6c31d59c3476601a0d4f Mon Sep 17 00:00:00 2001 From: Yao Li Date: Mon, 21 Dec 2020 16:17:56 -0600 Subject: [PATCH] Resolve #158. --- examples/containers/Makefile | 2 +- examples/containers/lib/_CoqProject | 2 +- examples/containers/theories/_CoqProject | 2 +- examples/core-semantics/Makefile | 2 +- examples/core-semantics/lib/_CoqProject | 2 +- examples/ghc/Makefile | 2 +- examples/ghc/lib/_CoqProject | 2 +- examples/ghc/theories/StateLogic.v | 2 +- examples/ghc/theories/_CoqProject | 2 +- examples/graph/Makefile | 2 +- .../graph/lib/Data/Graph/Inductive/Graph.v | 18 ++++++++---------- .../lib/Data/Graph/Inductive/Internal/Heap.v | 16 ++++++++-------- .../lib/Data/Graph/Inductive/Internal/Queue.v | 7 ++++--- examples/graph/lib/_CoqProject | 2 +- .../Data/Graph/Inductive/Graph/edits | 8 ++++---- .../Data/Graph/Inductive/Internal/Heap/edits | 8 ++++---- .../Data/Graph/Inductive/Internal/Queue/edits | 2 +- examples/graph/theories/_CoqProject | 2 +- examples/shuffle/Makefile | 2 +- examples/shuffle/theories/_CoqProject | 2 +- examples/transformers/Makefile | 2 +- examples/transformers/lib/_CoqProject | 2 +- 22 files changed, 45 insertions(+), 46 deletions(-) diff --git a/examples/containers/Makefile b/examples/containers/Makefile index b3f54aebb..ae108f33e 100644 --- a/examples/containers/Makefile +++ b/examples/containers/Makefile @@ -69,7 +69,7 @@ vfiles: $(OUT)/edits $(HS_SPEC)/README.md $(OUT)/README.md $(OUT)/_CoqProject $ $(OUT)/_CoqProject : Makefile $(OUT)/README.md > $@ echo '-Q . ""' >> $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo $(addsuffix .v,$(HANDMOD)) >> $@ echo $(addsuffix .v,$(MODULES)) >> $@ echo $(addsuffix .v,$(SPECIAL_MODULES)) >> $@ diff --git a/examples/containers/lib/_CoqProject b/examples/containers/lib/_CoqProject index ea9d24755..24483296b 100644 --- a/examples/containers/lib/_CoqProject +++ b/examples/containers/lib/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" Utils/Containers/Internal/PtrEquality.v CTZ.v BitTerminationProofs.v Test/QuickCheck/Property.v Test/QuickCheck/Arbitrary.v Test/QuickCheck/Gen.v IntWord.v Data/Set/Internal.v Utils/Containers/Internal/BitUtil.v Data/IntSet/Internal.v Data/IntSet/InternalWord.v Data/IntMap/Internal.v Data/Map/Internal.v IntSetValidity.v diff --git a/examples/containers/theories/_CoqProject b/examples/containers/theories/_CoqProject index 116835483..6406ad29e 100644 --- a/examples/containers/theories/_CoqProject +++ b/examples/containers/theories/_CoqProject @@ -1,6 +1,6 @@ -Q . "" -Q ../hs-spec "" --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../containers/lib "" CustomTactics.v diff --git a/examples/core-semantics/Makefile b/examples/core-semantics/Makefile index 8369d0bd9..e2c0380e6 100644 --- a/examples/core-semantics/Makefile +++ b/examples/core-semantics/Makefile @@ -33,7 +33,7 @@ vfiles: $(OUT)/edits $(OUT)/README.md $(OUT)/_CoqProject $(VFILES) $(OUT)/_CoqProject : $(OUT)/README.md Makefile > $@ echo '-Q . ""' >> $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo '-Q ../../../base-thy Proofs' >> $@ echo '-Q ../../containers/lib ""' >> $@ echo '-Q ../../containers/theories ""' >> $@ diff --git a/examples/core-semantics/lib/_CoqProject b/examples/core-semantics/lib/_CoqProject index 3ecae7f8e..2924bcc71 100644 --- a/examples/core-semantics/lib/_CoqProject +++ b/examples/core-semantics/lib/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../containers/lib "" -Q ../../containers/theories "" diff --git a/examples/ghc/Makefile b/examples/ghc/Makefile index 9777dfba8..8847bb8df 100644 --- a/examples/ghc/Makefile +++ b/examples/ghc/Makefile @@ -272,7 +272,7 @@ $(OUT)/edits: $(OUT)/_CoqProject: $(OUT)/README.md Makefile > $@ echo '-Q . ""' >> $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo '-Q ../../../base-thy Proofs' >> $@ echo '-Q ../../containers/lib ""' >> $@ echo '-Q ../../containers/theories ""' >> $@ diff --git a/examples/ghc/lib/_CoqProject b/examples/ghc/lib/_CoqProject index 82efa8e31..878c3f3e8 100644 --- a/examples/ghc/lib/_CoqProject +++ b/examples/ghc/lib/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../containers/lib "" -Q ../../containers/theories "" diff --git a/examples/ghc/theories/StateLogic.v b/examples/ghc/theories/StateLogic.v index 8beac348a..7b369e860 100644 --- a/examples/ghc/theories/StateLogic.v +++ b/examples/ghc/theories/StateLogic.v @@ -1,6 +1,6 @@ Require Import GHC.Base. Require State. -Require Traversable. +Require Data.Traversable. Set Bullet Behavior "Strict Subproofs". diff --git a/examples/ghc/theories/_CoqProject b/examples/ghc/theories/_CoqProject index b671d3c7b..1c0507c97 100644 --- a/examples/ghc/theories/_CoqProject +++ b/examples/ghc/theories/_CoqProject @@ -1,5 +1,5 @@ -Q . Proofs --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../ghc/lib "" -Q ../../transformers/lib "" diff --git a/examples/graph/Makefile b/examples/graph/Makefile index daf2ff8b3..c78f4edcd 100644 --- a/examples/graph/Makefile +++ b/examples/graph/Makefile @@ -68,7 +68,7 @@ vfiles: $(OUT)/edits $(HS_SPEC)/README.md $(OUT)/README.md $(OUT)/_CoqProject $ $(OUT)/_CoqProject : Makefile $(OUT)/README.md > $@ echo '-Q . ""' >> $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo '-Q ../../containers/lib ""' >> $@ echo $(addsuffix .v,$(HANDMOD)) >> $@ echo $(addsuffix .v,$(MODULES)) >> $@ diff --git a/examples/graph/lib/Data/Graph/Inductive/Graph.v b/examples/graph/lib/Data/Graph/Inductive/Graph.v index c9ac5e023..950c02076 100644 --- a/examples/graph/lib/Data/Graph/Inductive/Graph.v +++ b/examples/graph/lib/Data/Graph/Inductive/Graph.v @@ -28,7 +28,6 @@ Require Data.IntSet.Internal. Require Data.Maybe. Require Data.OldList. Require Data.Tuple. -Require Err. Require GHC.Base. Require GHC.Err. Require GHC.List. @@ -396,7 +395,7 @@ Definition insNode {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph : LNode a -> gr a b -> gr a b := fun '(pair v l) => (fun arg_1__ => pair (pair (pair nil v) l) nil & arg_1__). -Definition insEdge {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)} +Definition insEdge {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)} : LEdge b -> gr a b -> gr a b := fun arg_0__ arg_1__ => match arg_0__, arg_1__ with @@ -471,7 +470,7 @@ Definition insNodes {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph : list (LNode a) -> gr a b -> gr a b := fun vs g => Data.Foldable.foldl' (GHC.Base.flip insNode) g vs. -Definition insEdges {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)} +Definition insEdges {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)} : list (LEdge b) -> gr a b -> gr a b := fun es g => Data.Foldable.foldl' (GHC.Base.flip insEdge) g es. @@ -520,7 +519,7 @@ Definition subgraph {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph let vs' := Data.IntSet.Internal.fromList vs in nfilter (fun arg_1__ => Data.IntSet.Internal.member arg_1__ vs'). -Definition context {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)} +Definition context {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)} : gr a b -> Node -> Context a b := fun g v => Data.Maybe.fromMaybe (GHC.Err.error (Coq.Init.Datatypes.app @@ -609,7 +608,7 @@ Definition deg' {a : Type} {b : Type} : Context a b -> GHC.Num.Int := fun '(pair (pair (pair p _) _) s) => GHC.List.length p GHC.Num.+ GHC.List.length s. -Definition deg {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)} +Definition deg {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)} : gr a b -> Node -> GHC.Num.Int := deg' .: context. @@ -709,9 +708,8 @@ End Notations. Data.Function.on Data.IntSet.Internal.fromList Data.IntSet.Internal.member Data.Maybe.fromMaybe Data.Maybe.isJust Data.Maybe.maybe Data.OldList.delete Data.OldList.op_zrzr__ Data.OldList.sortBy Data.Tuple.fst Data.Tuple.snd - Err.Default GHC.Base.Eq_ GHC.Base.compare GHC.Base.flip GHC.Base.fmap - GHC.Base.hs_string__ GHC.Base.id GHC.Base.map GHC.Base.op_z2218U__ - GHC.Base.op_zeze__ GHC.Base.op_zsze__ GHC.Err.error GHC.List.elem - GHC.List.filter GHC.List.length GHC.Num.Int GHC.Num.op_zp__ GHC.Tuple.pair2 - String.EmptyString + GHC.Base.Eq_ GHC.Base.compare GHC.Base.flip GHC.Base.fmap GHC.Base.hs_string__ + GHC.Base.id GHC.Base.map GHC.Base.op_z2218U__ GHC.Base.op_zeze__ + GHC.Base.op_zsze__ GHC.Err.Default GHC.Err.error GHC.List.elem GHC.List.filter + GHC.List.length GHC.Num.Int GHC.Num.op_zp__ GHC.Tuple.pair2 String.EmptyString *) diff --git a/examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v b/examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v index 216215e2a..d2911975d 100644 --- a/examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v +++ b/examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v @@ -20,7 +20,6 @@ Require Import Wellfounded. Require Data.Foldable. Require Data.Tuple. -Require Err. Require GHC.Base. Require GHC.Err. Require List. @@ -87,7 +86,7 @@ Fixpoint mergeAll {a : Type} {b : Type} `{GHC.Base.Ord a} (arg_0__ Definition isEmpty {a : Type} {b : Type} : Heap a b -> bool := fun arg_0__ => match arg_0__ with | Empty => true | _ => false end. -Definition findMin {a} {b} `{Err.Default (a * b)} : Heap a b -> a * b := +Definition findMin {a} {b} `{GHC.Err.Default (a * b)} : Heap a b -> a * b := fun arg_0__ => match arg_0__ with | Empty => GHC.Err.error (GHC.Base.hs_string__ "Heap.findMin: empty heap") @@ -102,7 +101,8 @@ Definition deleteMin {a : Type} {b : Type} `{GHC.Base.Ord a} | Node _ _ hs => mergeAll hs end. -Definition splitMin {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b * Heap a b)} +Definition splitMin {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b * + Heap a b)} : Heap a b -> a * b * Heap a b := fun arg_0__ => match arg_0__ with @@ -158,7 +158,7 @@ Proof. intros. assert (A: h <> Empty) by auto; apply deleteMin_size in A; omega. Qed. -Program Fixpoint toList {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b)} +Program Fixpoint toList {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b)} (arg_0__ : Heap a b) {measure (size arg_0__)} : list (a * b) := match arg_0__ with | Empty => nil @@ -166,14 +166,14 @@ Program Fixpoint toList {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b)} end. Solve Obligations with ((Tactics.program_simpl; apply toList_termination; auto)). -Definition heapsort {a} `{GHC.Base.Ord a} `{Err.Default (a * a)} +Definition heapsort {a} `{GHC.Base.Ord a} `{GHC.Err.Default (a * a)} : list a -> list a := GHC.Base.map Data.Tuple.fst GHC.Base.∘ (toList GHC.Base.∘ (build GHC.Base.∘ GHC.Base.map (fun x => pair x x))). (* External variables: Type bool cons false list nil op_ze__ op_zl__ op_zlzg__ op_zp__ op_zt__ pair - plus true Data.Foldable.foldr Data.Tuple.fst Err.Default GHC.Base.Ord - GHC.Base.map GHC.Base.op_z2218U__ GHC.Base.op_zl__ GHC.Err.error List.fold_right - List.map Nat.add + plus true Data.Foldable.foldr Data.Tuple.fst GHC.Base.Ord GHC.Base.map + GHC.Base.op_z2218U__ GHC.Base.op_zl__ GHC.Err.Default GHC.Err.error + List.fold_right List.map Nat.add *) diff --git a/examples/graph/lib/Data/Graph/Inductive/Internal/Queue.v b/examples/graph/lib/Data/Graph/Inductive/Internal/Queue.v index 8e7873b51..f7da2ba45 100644 --- a/examples/graph/lib/Data/Graph/Inductive/Internal/Queue.v +++ b/examples/graph/lib/Data/Graph/Inductive/Internal/Queue.v @@ -13,9 +13,9 @@ Require Coq.Program.Wf. (* Converted imports: *) Require Data.Foldable. -Require Err. Require GHC.Base. Require GHC.DeferredFix. +Require GHC.Err. Require GHC.List. (* Converted type declarations: *) @@ -38,7 +38,8 @@ Definition queuePut {a : Type} : a -> Queue a -> Queue a := Definition queuePutList {a : Type} : list a -> Queue a -> Queue a := fun xs q => Data.Foldable.foldl' (GHC.Base.flip queuePut) q xs. -Definition queueGet {a} `{Err.Default (a * Queue a)} : Queue a -> a * Queue a := +Definition queueGet {a} `{GHC.Err.Default (a * Queue a)} + : Queue a -> a * Queue a := GHC.DeferredFix.deferredFix1 (fun queueGet (arg_0__ : Queue a) => match arg_0__ with | MkQueue ins (cons item rest) => pair item (MkQueue ins rest) @@ -51,6 +52,6 @@ Definition queueEmpty {a : Type} : Queue a -> bool := (* External variables: Type andb bool cons list nil op_zt__ pair Data.Foldable.foldl' - Data.Foldable.null Err.Default GHC.Base.flip GHC.DeferredFix.deferredFix1 + Data.Foldable.null GHC.Base.flip GHC.DeferredFix.deferredFix1 GHC.Err.Default GHC.List.reverse *) diff --git a/examples/graph/lib/_CoqProject b/examples/graph/lib/_CoqProject index 332d6a893..302c69791 100644 --- a/examples/graph/lib/_CoqProject +++ b/examples/graph/lib/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" -Q ../../containers/lib "" Data/Graph/Inductive/Graph.v Data/Graph/Inductive/Internal/Queue.v Data/Graph/Inductive/Internal/RootPath.v Data/Graph/Inductive/Internal/Heap.v Data/Graph/Inductive/Query/BFS.v Data/Graph/Inductive/Query/SP.v diff --git a/examples/graph/module-edits/Data/Graph/Inductive/Graph/edits b/examples/graph/module-edits/Data/Graph/Inductive/Graph/edits index 0445f0813..40f932fbf 100644 --- a/examples/graph/module-edits/Data/Graph/Inductive/Graph/edits +++ b/examples/graph/module-edits/Data/Graph/Inductive/Graph/edits @@ -29,10 +29,10 @@ in Data.Graph.Inductive.Graph.lab rewrite forall, GHC.Base.fmap = (@GHC.Base.fma rewrite forall s, (GHC.Show.show s) = (GHC.Base.hs_string__ String.EmptyString) #need some Default constraints -set type Data.Graph.Inductive.Graph.insEdge : forall {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}, (LEdge b) -> ((gr a b) -> (gr a b)) -set type Data.Graph.Inductive.Graph.insEdges : forall {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}, list (LEdge b) -> ((gr a b) -> (gr a b)) -set type Data.Graph.Inductive.Graph.context: forall {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}, (gr a b) -> (Node -> (Context a b)) -set type Data.Graph.Inductive.Graph.deg: forall {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}, (gr a b) -> (Node -> GHC.Num.Int) +set type Data.Graph.Inductive.Graph.insEdge : forall {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}, (LEdge b) -> ((gr a b) -> (gr a b)) +set type Data.Graph.Inductive.Graph.insEdges : forall {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}, list (LEdge b) -> ((gr a b) -> (gr a b)) +set type Data.Graph.Inductive.Graph.context: forall {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}, (gr a b) -> (Node -> (Context a b)) +set type Data.Graph.Inductive.Graph.deg: forall {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}, (gr a b) -> (Node -> GHC.Num.Int) #Coq gets confused about some polymorphic definitions in Data.Graph.Inductive.Graph.hasNeighborAdj rewrite forall, Data.Foldable.elem = GHC.List.elem diff --git a/examples/graph/module-edits/Data/Graph/Inductive/Internal/Heap/edits b/examples/graph/module-edits/Data/Graph/Inductive/Internal/Heap/edits index 479cad832..e45023c2a 100644 --- a/examples/graph/module-edits/Data/Graph/Inductive/Internal/Heap/edits +++ b/examples/graph/module-edits/Data/Graph/Inductive/Internal/Heap/edits @@ -2,8 +2,8 @@ skip Data.Graph.Inductive.Internal.Heap.prettyHeap skip Data.Graph.Inductive.Internal.Heap.printPrettyHeap #needs default as well for some reason -set type Data.Graph.Inductive.Internal.Heap.splitMin: forall {a} {b} `{GHC.Base.Ord a} `{Err.Default ((a * b) * (Heap a b))}, (Heap a b) -> ((a * b) * (Heap a b)) -set type Data.Graph.Inductive.Internal.Heap.findMin: forall {a} {b} `{Err.Default (a * b)}, (Heap a b) -> (a * b) +set type Data.Graph.Inductive.Internal.Heap.splitMin: forall {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default ((a * b) * (Heap a b))}, (Heap a b) -> ((a * b) * (Heap a b)) +set type Data.Graph.Inductive.Internal.Heap.findMin: forall {a} {b} `{GHC.Err.Default (a * b)}, (Heap a b) -> (a * b) #need to prove that toList terminates - we need a function for the size of a heap add Data.Graph.Inductive.Internal.Heap Fixpoint Data.Graph.Inductive.Internal.Heap.size {a} {b} (h: Heap a b) := @@ -56,8 +56,8 @@ termination Data.Graph.Inductive.Internal.Heap.toList {measure (Data.Grap obligations Data.Graph.Inductive.Internal.Heap.toList (Tactics.program_simpl; apply toList_termination; auto) #more defaut constrants -set type Data.Graph.Inductive.Internal.Heap.toList: forall {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b)}, (Heap a b) -> list (a * b) -set type Data.Graph.Inductive.Internal.Heap.heapsort: forall {a} `{GHC.Base.Ord a} `{Err.Default (a * a)}, list a -> list a +set type Data.Graph.Inductive.Internal.Heap.toList: forall {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b)}, (Heap a b) -> list (a * b) +set type Data.Graph.Inductive.Internal.Heap.heapsort: forall {a} `{GHC.Base.Ord a} `{GHC.Err.Default (a * a)}, list a -> list a #recursive definition that is difficult to translate skip class GHC.Base.Ord diff --git a/examples/graph/module-edits/Data/Graph/Inductive/Internal/Queue/edits b/examples/graph/module-edits/Data/Graph/Inductive/Internal/Queue/edits index 899215353..3c39ad1ed 100644 --- a/examples/graph/module-edits/Data/Graph/Inductive/Internal/Queue/edits +++ b/examples/graph/module-edits/Data/Graph/Inductive/Internal/Queue/edits @@ -1,3 +1,3 @@ #does not terminate on empty queue -set type Data.Graph.Inductive.Internal.Queue.queueGet: forall {a} `{Err.Default (a * Queue a)}, Queue a -> (a * Queue a) +set type Data.Graph.Inductive.Internal.Queue.queueGet: forall {a} `{GHC.Err.Default (a * Queue a)}, Queue a -> (a * Queue a) termination Data.Graph.Inductive.Internal.Queue.queueGet deferred diff --git a/examples/graph/theories/_CoqProject b/examples/graph/theories/_CoqProject index 65b72679d..9ade91b84 100644 --- a/examples/graph/theories/_CoqProject +++ b/examples/graph/theories/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../graph/lib "" -Q ../../containers/lib "" diff --git a/examples/shuffle/Makefile b/examples/shuffle/Makefile index 77cc9639a..cd905ebfd 100644 --- a/examples/shuffle/Makefile +++ b/examples/shuffle/Makefile @@ -22,7 +22,7 @@ coq: $(OUT)/Makefile $(OUT)/_CoqProject: $(OUT) Makefile mkdir -p $(OUT) echo '-Q . ""' > $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo '-Q ../../containers/lib ""' >> $@ echo '-Q ../../transformers/lib ""' >> $@ (cd $(OUT) && find . -name '*.v') >> $@ diff --git a/examples/shuffle/theories/_CoqProject b/examples/shuffle/theories/_CoqProject index 8061d13b3..35ddb6878 100644 --- a/examples/shuffle/theories/_CoqProject +++ b/examples/shuffle/theories/_CoqProject @@ -1,6 +1,6 @@ -Q . Proofs --R ../../../base "" +-Q ../../../base "" -Q ../../../base-thy Proofs -Q ../../transformers/lib "" diff --git a/examples/transformers/Makefile b/examples/transformers/Makefile index b5b409f99..886f7c517 100644 --- a/examples/transformers/Makefile +++ b/examples/transformers/Makefile @@ -72,7 +72,7 @@ $(OUT)/_CoqProject : Makefile mkdir -p $(OUT) > $@ echo '-Q . ""' >> $@ - echo '-R ../../../base ""' >> $@ + echo '-Q ../../../base ""' >> $@ echo $(addsuffix .v,$(HANDMOD)) >> $@ echo $(addsuffix .v,$(MODULES)) >> $@ echo $(addsuffix .v,$(SPECIAL_MODULES)) >> $@ diff --git a/examples/transformers/lib/_CoqProject b/examples/transformers/lib/_CoqProject index 6a2d13194..57f4fdb1c 100644 --- a/examples/transformers/lib/_CoqProject +++ b/examples/transformers/lib/_CoqProject @@ -1,5 +1,5 @@ -Q . "" --R ../../../base "" +-Q ../../../base "" Data/Functor/Constant.v Data/Functor/Reverse.v Control/Applicative/Backwards.v Control/Applicative/Lift.v Control/Monad/Trans/Class.v Control/Monad/Signatures.v Control/Monad/Trans/Identity.v Control/Monad/Trans/Reader.v Control/Monad/Trans/Writer/Lazy.v Control/Monad/Trans/State/Lazy.v Control/Monad/Trans/Cont.v Control/Monad/Trans/Except.v Control/Monad/Trans/Maybe.v Control/Monad/Trans/RWS/Lazy.v