diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean
index 1af2053cf4..ff8cbcbe9b 100644
--- a/library/init/lean/declaration.lean
+++ b/library/init/lean/declaration.lean
@@ -94,50 +94,55 @@ structure recursor_val extends declaration_val :=
 (rules : list recursor_rule) -- A reduction for each constructor
 (is_meta : bool)
 
-inductive declaration
-| axiom_decl  (val : axiom_val)
-| defn_decl   (val : definition_val)
-| thm_decl    (val : theorem_val)
-| induct_decl (val : inductive_val)
-| cnstr_decl  (val : constructor_val)
-| rec_decl    (val : recursor_val)
+inductive quot_kind
+| type  -- `quot`
+| cnstr -- `quot.mk`
+| lift  -- `quot.lift`
+| ind   -- `quot.ind`
 
-namespace declaration
+structure quot_val extends declaration_val :=
+(kind : quot_kind)
 
-def to_declaration_val : declaration → declaration_val
-| (defn_decl   {to_declaration_val := d, ..}) := d
-| (axiom_decl  {to_declaration_val := d, ..}) := d
-| (thm_decl    {to_declaration_val := d, ..}) := d
-| (induct_decl {to_declaration_val := d, ..}) := d
-| (cnstr_decl  {to_declaration_val := d, ..}) := d
-| (rec_decl    {to_declaration_val := d, ..}) := d
+/-- Information associated with constant declarations. -/
+inductive constant_info
+| axiom_info    (val : axiom_val)
+| defn_info     (val : definition_val)
+| thm_info      (val : theorem_val)
+| quot_info     (val : quot_val)
+| induct_info   (val : inductive_val)
+| cnstr_info    (val : constructor_val)
+| rec_info      (val : recursor_val)
 
-def id (d : declaration) : name :=
+namespace constant_info
+
+def to_declaration_val : constant_info → declaration_val
+| (defn_info     {to_declaration_val := d, ..}) := d
+| (axiom_info    {to_declaration_val := d, ..}) := d
+| (thm_info      {to_declaration_val := d, ..}) := d
+| (quot_info     {to_declaration_val := d, ..}) := d
+| (induct_info   {to_declaration_val := d, ..}) := d
+| (cnstr_info    {to_declaration_val := d, ..}) := d
+| (rec_info      {to_declaration_val := d, ..}) := d
+
+def id (d : constant_info) : name :=
 d.to_declaration_val.id
 
-def lparams (d : declaration) : list name :=
+def lparams (d : constant_info) : list name :=
 d.to_declaration_val.lparams
 
-def type (d : declaration) : expr :=
+def type (d : constant_info) : expr :=
 d.to_declaration_val.type
 
-def value : declaration → option expr
-| (defn_decl {value := r, ..}) := some r
-| (thm_decl  {value := r, ..}) := some r
+def value : constant_info → option expr
+| (defn_info {value := r, ..}) := some r
+| (thm_info  {value := r, ..}) := some r
 | _                            := none
 
-def hints : declaration → reducibility_hints
-| (defn_decl {hints := r, ..}) := r
+def hints : constant_info → reducibility_hints
+| (defn_info {hints := r, ..}) := r
 | _                            := reducibility_hints.opaque
 
-def is_meta : declaration → bool
-| (defn_decl   {is_meta := r, ..}) := r
-| (induct_decl {is_meta := r, ..}) := r
-| (cnstr_decl  {is_meta := r, ..}) := r
-| (rec_decl    {is_meta := r, ..}) := r
-| _                                := ff
-
-end declaration
+end constant_info
 
 structure constructor :=
 (id : name) (type : expr)
diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean
index 07ac0a3545..c9e87eca9b 100644
--- a/library/init/meta/declaration.lean
+++ b/library/init/meta/declaration.lean
@@ -6,16 +6,16 @@ Authors: Leonardo de Moura
 prelude
 import init.lean.declaration
 
-export lean (declaration reducibility_hints)
+export lean (constant_info reducibility_hints)
 
 namespace lean
-namespace declaration
+namespace constant_info
 
 /-- Instantiate a universe polymorphic declaration type with the given universes. -/
-meta constant instantiate_type_univ_params : declaration → list level → option expr
+meta constant instantiate_type_univ_params : constant_info → list level → option expr
 
 /-- Instantiate a universe polymorphic declaration value with the given universes. -/
-meta constant instantiate_value_univ_params : declaration → list level → option expr
+meta constant instantiate_value_univ_params : constant_info → list level → option expr
 
-end declaration
+end constant_info
 end lean
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index 8a80a924cd..e920bf36ca 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -26,10 +26,10 @@ structure projection_info :=
 meta constant mk_std          : nat → environment
 /-- Return the trust level of the given environment -/
 meta constant trust_lvl       : environment → nat
-/-- Add a new declaration to the environment -/
-meta constant add             : environment → declaration → exceptional environment
+-- /-- Add a new declaration to the environment -/
+-- meta constant add             : environment → declaration → exceptional environment
 /-- Retrieve a declaration from the environment -/
-meta constant get             : environment → name → exceptional declaration
+meta constant get             : environment → name → exceptional constant_info
 meta def      contains (env : environment) (d : name) : bool :=
 match env.get d with
 | exceptional.success _     := tt
@@ -67,7 +67,7 @@ meta constant inductive_dep_elim : environment → name → bool
 meta constant is_ginductive : environment → name → bool
 meta constant is_projection : environment → name → option projection_info
 /-- Fold over declarations in the environment -/
-meta constant fold {α :Type} : environment → α → (declaration → α → α) → α
+meta constant fold {α :Type} : environment → α → (constant_info → α → α) → α
 /-- `relation_info env n` returns some value if n is marked as a relation in the given environment.
    the tuple contains: total number of arguments of the relation, lhs position and rhs position. -/
 meta constant relation_info : environment → name → option (nat × nat × nat)
@@ -107,8 +107,8 @@ meta def in_current_file (env : environment) (n : name) : bool :=
 
 meta def is_definition (env : environment) (n : name) : bool :=
 match env.get n with
-| exceptional.success (lean.declaration.defn_decl _) := tt
-| _                                                  := ff
+| exceptional.success (lean.constant_info.defn_info _) := tt
+| _                                                    := ff
 
 end environment
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 7b9dab332a..0651eb4e3c 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -209,7 +209,7 @@ meta def get_env : tactic environment :=
 do s ← read,
    return $ env s
 
-meta def get_decl (n : name) : tactic declaration :=
+meta def get_decl (n : name) : tactic constant_info :=
 do s ← read,
    (env s).get n
 
@@ -412,8 +412,8 @@ meta constant destruct (e : expr) (md := semireducible) : tactic unit
 meta constant generalize (e : expr) (n : name := `_x) (md := semireducible) : tactic unit
 /-- instantiate assigned metavariables in the given expression -/
 meta constant instantiate_mvars : expr → tactic expr
-/-- Add the given declaration to the environment -/
-meta constant add_decl : declaration → tactic unit
+-- /-- Add the given declaration to the environment -/
+-- meta constant add_decl : declaration → tactic unit
 /-- Changes the environment to the `new_env`. `new_env` needs to be a descendant from the current environment. -/
 meta constant set_env : environment → tactic unit
 /-- (doc_string env d k) return the doc string for d (if available) -/
@@ -1054,8 +1054,8 @@ meta def add_inductive (n : name) (ls : list name) (p : nat) (ty : expr) (is : l
   (is_meta : bool := ff) : tactic unit :=
 updateex_env $ λe, e.add_inductive n ls p ty is is_meta
 
-meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit :=
-add_decl (lean.declaration.defn_decl { id := n, lparams := lvls, type := type, value := value, hints := lean.reducibility_hints.abbrev, is_meta := tt })
+-- meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit :=
+-- add_decl (lean.declaration.defn_decl { id := n, lparams := lvls, type := type, value := value, hints := lean.reducibility_h-- ints.abbrev, is_meta := tt })
 
 meta def rename (curr : name) (new : name) : tactic unit :=
 do h ← get_local curr,
diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp
index 615ce4bc0b..f693885979 100644
--- a/src/library/vm/vm_declaration.cpp
+++ b/src/library/vm/vm_declaration.cpp
@@ -132,12 +132,12 @@ vm_obj declaration_instantiate_value_univ_params(vm_obj const & _d, vm_obj const
 }
 
 void initialize_vm_declaration() {
-    DECLARE_VM_BUILTIN(name({"lean", "declaration", "defn_decl"}),  declaration_defn);
-    DECLARE_VM_BUILTIN(name({"lean", "declaration", "thm_decl"}),   declaration_thm);
-    DECLARE_VM_BUILTIN(name({"lean", "declaration", "axion_decl"}), declaration_ax);
-    DECLARE_VM_BUILTIN(name({"lean", "declaration", "instantiate_type_univ_params"}),  declaration_instantiate_type_univ_params);
-    DECLARE_VM_BUILTIN(name({"lean", "declaration", "instantiate_value_univ_params"}), declaration_instantiate_value_univ_params);
-    DECLARE_VM_CASES_BUILTIN(name({"lean", "declaration", "cases_on"}), declaration_cases_on);
+    DECLARE_VM_BUILTIN(name({"lean", "constant_info", "defn_info"}),  declaration_defn);
+    DECLARE_VM_BUILTIN(name({"lean", "constant_info", "thm_info"}),   declaration_thm);
+    DECLARE_VM_BUILTIN(name({"lean", "constant_info", "axiom_info"}), declaration_ax);
+    DECLARE_VM_BUILTIN(name({"lean", "constant_info", "instantiate_type_univ_params"}),  declaration_instantiate_type_univ_params);
+    DECLARE_VM_BUILTIN(name({"lean", "constant_info", "instantiate_value_univ_params"}), declaration_instantiate_value_univ_params);
+    DECLARE_VM_CASES_BUILTIN(name({"lean", "constant_info", "cases_on"}), declaration_cases_on);
 }
 
 void finalize_vm_declaration() {
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 3efd7b90e9..2dd0709e43 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -58,6 +58,7 @@ vm_obj environment_trust_lvl(vm_obj const & env) {
     return mk_vm_nat(to_env(env).trust_lvl());
 }
 
+/*
 vm_obj environment_add(vm_obj const & env, vm_obj const & decl) {
     try {
         return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl)))));
@@ -65,6 +66,7 @@ vm_obj environment_add(vm_obj const & env, vm_obj const & decl) {
         return mk_vm_exceptional_exception(std::current_exception());
     }
 }
+*/
 
 vm_obj environment_get(vm_obj const & env, vm_obj const & n) {
     try {
@@ -253,7 +255,7 @@ vm_obj environment_fingerprint(vm_obj const & env) {
 void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "mk_std"}),                environment_mk_std);
     DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}),             environment_trust_lvl);
-    DECLARE_VM_BUILTIN(name({"environment", "add"}),                   environment_add);
+    // DECLARE_VM_BUILTIN(name({"environment", "add"}),                   environment_add);
     DECLARE_VM_BUILTIN(name({"environment", "get"}),                   environment_get);
     DECLARE_VM_BUILTIN(name({"environment", "fold"}),                  environment_fold);
     DECLARE_VM_BUILTIN(name({"environment", "add_inductive"}),         environment_add_inductive);