From e2bfe6ee364d58b8d5eb5dc05d65eeaabdf9bdce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Nov 2014 16:12:44 -0800
Subject: [PATCH] refactor(library/definitional/no_confusion): cleanup API

---
 src/frontends/lean/inductive_cmd.cpp      | 14 +++++++++-----
 src/library/definitional/no_confusion.cpp |  6 +++---
 src/library/definitional/no_confusion.h   |  2 +-
 3 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index fb9509844..e0ac89719 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -637,6 +637,12 @@ struct inductive_cmd_fn {
         m_decl_info.emplace_back(n, *g_definition, pos);
     }
 
+    void save_if_defined(name const & n, pos_info pos) {
+        if (m_env.find(n)) {
+            m_decl_info.emplace_back(n, *g_definition, pos);
+        }
+    }
+
     environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
         bool has_unit = has_unit_decls(env);
         bool has_eq   = has_eq_decls(env);
@@ -653,11 +659,9 @@ struct inductive_cmd_fn {
                 env = mk_cases_on(env, inductive_decl_name(d));
                 save_def_info(name(n, "cases_on"), pos);
                 if (has_eq && has_heq) {
-                    if (optional<environment> new_env = mk_no_confusion(env, inductive_decl_name(d))) {
-                       env = *new_env;
-                       save_def_info(name{n, "no_confusion_type"}, pos);
-                       save_def_info(name(n, "no_confusion"), pos);
-                    }
+                    env = mk_no_confusion(env, inductive_decl_name(d));
+                    save_if_defined(name{n, "no_confusion_type"}, pos);
+                    save_if_defined(name(n, "no_confusion"), pos);
                 }
                 // if (has_prod) {
                 //    env = mk_below(env, inductive_decl_name(d));
diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index e0fab1d62..c4a35fbea 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -138,10 +138,10 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     return some(add_protected(new_env, no_confusion_type_name));
 }
 
-optional<environment> mk_no_confusion(environment const & env, name const & n) {
+environment mk_no_confusion(environment const & env, name const & n) {
     optional<environment> env1 = mk_no_confusion_type(env, n);
     if (!env1)
-        return env1;
+        return env;
     environment new_env = *env1;
     type_checker tc(new_env);
     inductive::inductive_decls decls   = *inductive::is_inductive_decl(new_env, n);
@@ -256,6 +256,6 @@ optional<environment> mk_no_confusion(environment const & env, name const & n) {
     declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
                                       opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
     new_env = module::add(new_env, check(new_env, new_d));
-    return some(add_protected(new_env, no_confusion_name));
+    return add_protected(new_env, no_confusion_name);
 }
 }
diff --git a/src/library/definitional/no_confusion.h b/src/library/definitional/no_confusion.h
index 0d7a2713b..dff08b184 100644
--- a/src/library/definitional/no_confusion.h
+++ b/src/library/definitional/no_confusion.h
@@ -15,5 +15,5 @@ namespace lean {
 
     \remark Return none if did not create constructions because type is a proposition.
 */
-optional<environment> mk_no_confusion(environment const & env, name const & n);
+environment mk_no_confusion(environment const & env, name const & n);
 }