From d79b2babd31f11b3e218e32a484dcda401b39da4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2013 08:46:47 -0800
Subject: [PATCH] fix(*): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp               | 14 +++++++-------
 src/library/placeholder.cpp                 |  4 ++--
 src/library/placeholder.h                   |  2 +-
 src/tests/kernel/metavar.cpp                |  2 +-
 src/tests/library/elaborator/elaborator.cpp |  2 +-
 5 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9f7c17f84..a0a87637b 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -448,7 +448,7 @@ class parser::imp {
             unsigned i = 0;
             for (unsigned j = 0; j < imp_args.size(); j++) {
                 if (imp_args[j]) {
-                    new_args.push_back(save(mk_placholder(), pos));
+                    new_args.push_back(save(mk_placeholder(), pos));
                 } else {
                     if (i >= num_args)
                         throw parser_error(sstream() << "unexpected number of arguments for denotation with implicit arguments, it expects " << num_args << " explicit argument(s)", pos);
@@ -598,7 +598,7 @@ class parser::imp {
                     // get all explicit arguments.
                     for (unsigned i = 0; i < imp_args.size(); i++) {
                         if (imp_args[i]) {
-                            args.push_back(save(mk_placholder(), pos()));
+                            args.push_back(save(mk_placeholder(), pos()));
                         } else {
                             args.push_back(parse_expr(1));
                         }
@@ -763,7 +763,7 @@ class parser::imp {
             if (type)
                 arg_type = lift_free_vars(type, i);
             else
-                arg_type = save(mk_placholder(), names[i].first);
+                arg_type = save(mk_placeholder(), names[i].first);
             result[sz + i] = std::make_tuple(names[i].first, names[i].second, arg_type, implicit_decl);
         }
     }
@@ -960,7 +960,7 @@ class parser::imp {
     expr parse_placeholder() {
         auto p = pos();
         next();
-        return save(mk_placholder(), p);
+        return save(mk_placeholder(), p);
     }
 
     /**
@@ -1184,7 +1184,7 @@ class parser::imp {
             next();
             pre_type = parse_expr();
             if (!is_definition && curr_is_period()) {
-                pre_val  = save(mk_placholder(), pos());
+                pre_val  = save(mk_placeholder(), pos());
             } else {
                 check_assign_next("invalid definition, ':=' expected");
                 pre_val  = parse_expr();
@@ -1192,7 +1192,7 @@ class parser::imp {
         } else if (is_definition && curr_is_assign()) {
             auto p   = pos();
             next();
-            pre_type = save(mk_placholder(), p);
+            pre_type = save(mk_placeholder(), p);
             pre_val  = parse_expr();
         } else {
             mk_scope scope(*this);
@@ -1201,7 +1201,7 @@ class parser::imp {
             expr type_body = parse_expr();
             pre_type  = mk_abstraction(false, bindings, type_body);
             if (!is_definition && curr_is_period()) {
-                pre_val = mk_abstraction(true, bindings, mk_placholder());
+                pre_val = mk_abstraction(true, bindings, mk_placeholder());
             } else {
                 check_assign_next("invalid definition, ':=' expected");
                 expr val_body  = parse_expr();
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 2e6fdcd09..5ef37e050 100644
--- a/src/library/placeholder.cpp
+++ b/src/library/placeholder.cpp
@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_placeholder_name("_");
-expr mk_placholder() {
+expr mk_placeholder() {
     return mk_constant(g_placeholder_name);
 }
 
@@ -21,7 +21,7 @@ bool is_placeholder(expr const & e) {
 }
 
 bool has_placeholder(expr const & e) {
-    return occurs(mk_placholder(), e);
+    return occurs(mk_placeholder(), e);
 }
 
 class replace_placeholders_with_metavars_proc : public replace_visitor {
diff --git a/src/library/placeholder.h b/src/library/placeholder.h
index 7e2e936fa..6d0939e4b 100644
--- a/src/library/placeholder.h
+++ b/src/library/placeholder.h
@@ -14,7 +14,7 @@ class metavar_env;
     \brief Return a new placeholder expression. To be able to track location,
     a new constant for each placeholder.
 */
-expr mk_placholder();
+expr mk_placeholder();
 
 /**
     \brief Return true iff the given expression is a placeholder.
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 49beab810..06ad8a67c 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -446,7 +446,7 @@ static void tst21() {
                    add_lift(m1, 1, 7));
 }
 
-#define _ mk_placholder()
+#define _ mk_placeholder()
 
 static void tst22() {
     metavar_env menv;
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index 899c29d52..b066c19e3 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -266,7 +266,7 @@ static void tst6() {
     std::cout << instantiate_metavars(V, s) << "\n";
 }
 
-#define _ mk_placholder()
+#define _ mk_placeholder()
 
 static expr elaborate(expr const & e, environment const & env) {
     metavar_env menv;