Browse files

rearrange cabal fields

  • Loading branch information...
1 parent 89bf54c commit 491515a527836ba6f3d3cdf631ec307c69c1ff01 @gwern gwern committed Mar 12, 2008
Showing with 17 additions and 6 deletions.
  1. +17 −6 ivor.cabal
@@ -1,12 +1,14 @@
Name: ivor
-Version: 0.1.6
+Version: 0.1.5
Author: Edwin Brady
License: BSD3
License-file: LICENSE
+Author: Edwin Brady
+Maintainer: Edwin Brady <>
Stability: experimental
-Build-depends: base, haskell98, parsec, mtl, directory, containers
+Build-depends: base, haskell98, parsec, mtl, plugins
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances
Synopsis: Theorem proving library based on dependent type theory
@@ -18,6 +20,7 @@ Description: Ivor is a type theory based theorem prover, with a
less along the lines of systems such as Coq or Agda,
and taking much of its inspiration from Conor
McBride's presentation of OLEG.
+ .
The API provides a collection of primitive tactics and
combinators for building new tactics. It is therefore
possible to build new tactics to suit specific
@@ -30,12 +33,20 @@ Description: Ivor is a type theory based theorem prover, with a
new parser rules, user defined tactics and (if you
want your proofs to be untrustworthy) a fixpoint
-Category: Theorem provers
+Build-depends: base, haskell98, parsec, mtl, plugins, directory
+Build-type: Simple
+Extensions: MultiParamTypeClasses, FunctionalDependencies,
+ ExistentialQuantification, OverlappingInstances
+-- Needs some -Wall cleanup
+-- GHC-options: -Wall
- Ivor.TT, Ivor.Shell, Ivor.Primitives,
+ Ivor.TT, Ivor.Shell, Ivor.Primitives,
Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality,
Ivor.Plugin, Ivor.Construction
-Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
+Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator
Ivor.Gadgets, Ivor.SC, Ivor.Bytecode,
Ivor.CodegenC, Ivor.Datatype, Ivor.Display,

0 comments on commit 491515a

Please sign in to comment.