diff --git a/ChangeLog b/ChangeLog
index ef8a6e689..3716d56fa 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,17 @@
 2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* src/ltlenv/environment.hh (require): Return a formula, not
+	an atomic_prop.
+	* src/ltlast/atomic_prop.hh (atomic_prop): New argument env.
+	(environment_): New member.
+	(env): New method.
+	* src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise.
+	* src/ltlenv/defaultenv.cc (require): Pass *this as the
+	environment argument to atomic_prop.
+	* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy 
+	the environment.
+	* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
+	
 	* configure.ac: Output src/ltlenv/Makefile.
 	* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
 	src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index d381e29b2..70bd1cccf 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -6,8 +6,8 @@ namespace spot
   namespace ltl
   {
  
-    atomic_prop::atomic_prop(std::string name)
-      : name_(name)
+    atomic_prop::atomic_prop(const std::string& name, environment& env)
+      : name_(name), env_(&env)
     {
     }
 
@@ -32,5 +32,12 @@ namespace spot
     {
       return name_;
     }
+    
+    environment& 
+    atomic_prop::env() const
+    {
+      return *env_;
+    }
+
   }
 }
diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh
index a8fefc511..5b5ec078e 100644
--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@@ -3,6 +3,7 @@
 
 #include <string>
 #include "formula.hh"
+#include "ltlenv/environment.hh"
 
 namespace spot
 {
@@ -12,15 +13,17 @@ namespace spot
     class atomic_prop : public formula
     {
     public:
-      atomic_prop(std::string name);
+      atomic_prop(const std::string& name, environment& env);
       virtual ~atomic_prop();
 
       virtual void accept(visitor& visitor);
       virtual void accept(const_visitor& visitor) const;
 
       const std::string& name() const;
+      environment& env() const;
     private:
       std::string name_;
+      environment* env_;
     };
 
   }
diff --git a/src/ltlenv/defaultenv.cc b/src/ltlenv/defaultenv.cc
index 03bd64520..4db008f10 100644
--- a/src/ltlenv/defaultenv.cc
+++ b/src/ltlenv/defaultenv.cc
@@ -5,10 +5,10 @@ namespace spot
   namespace ltl
   {
 
-    atomic_prop*
+    formula*
     default_environment::require(const std::string& s)
     {
-      return new atomic_prop(s);
+      return new atomic_prop(s, *this);
     }
 
     const std::string&
diff --git a/src/ltlenv/defaultenv.hh b/src/ltlenv/defaultenv.hh
index d8266feb0..db4010e3e 100644
--- a/src/ltlenv/defaultenv.hh
+++ b/src/ltlenv/defaultenv.hh
@@ -2,6 +2,7 @@
 # define SPOT_LTLENV_DEFAULT_ENVIRONMENT_HH
 
 # include "environment.hh"
+# include "ltlast/atomic_prop.hh"
 
 namespace spot
 {
@@ -11,7 +12,7 @@ namespace spot
     class default_environment : public environment
     {
     public:
-      virtual atomic_prop* require(const std::string& prop_str);
+      virtual formula* require(const std::string& prop_str);
       virtual const std::string& name();
 
       /* This class is a singleton.  */
diff --git a/src/ltlenv/environment.hh b/src/ltlenv/environment.hh
index 3e70fea2d..859c68051 100644
--- a/src/ltlenv/environment.hh
+++ b/src/ltlenv/environment.hh
@@ -1,7 +1,7 @@
 #ifndef SPOT_LTLENV_ENVIRONMENT_HH
 # define SPOT_LTLENV_ENVIRONMENT_HH
 
-# include "ltlast/atomic_prop.hh"
+# include "ltlast/formula.hh"
 # include <string>
 
 namespace spot
@@ -16,7 +16,11 @@ namespace spot
       // described by prop_str.
       // Note this is NOT a const method.  Some environment will
       // "create" the atomic proposition when asked.
-      virtual atomic_prop* require(const std::string& prop_str) = 0; 
+      // We return a formula instead of an atomic_prop, because this
+      // will allow nifty tricks (e.g., we could name formulae in an
+      // environment, and let the parser build a larger tree from
+      // these).
+      virtual formula* require(const std::string& prop_str) = 0; 
 
       virtual const std::string& name() = 0;
       // FIXME: More functions will be needed later, but
diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc
index 4389029eb..ff27625d5 100644
--- a/src/ltlvisit/clone.cc
+++ b/src/ltlvisit/clone.cc
@@ -22,7 +22,7 @@ namespace spot
     void 
     clone_visitor::visit(const atomic_prop* ap)
     {
-      result_ = new atomic_prop(ap->name());
+      result_ = new atomic_prop(ap->name(), ap->env());
     }
 
     void 
diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc
index 4a0d85e8c..153c505a8 100644
--- a/src/ltlvisit/nenoform.cc
+++ b/src/ltlvisit/nenoform.cc
@@ -27,7 +27,7 @@ namespace spot
       void 
       visit(const atomic_prop* ap)
       {
-	formula* f = new atomic_prop(ap->name());
+	formula* f = new atomic_prop(ap->name(), ap->env());
 	if (negated_)
 	  result_ = new unop(unop::Not, f);
 	else