From 8c2cb44ac0885a244b93cb02e37af4836724377d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Dec 2020 17:40:18 -0800
Subject: [PATCH] fix: error message produced by `lean_mk_projections`

---
 src/Lean/Elab/Structure.lean             | 6 +++---
 src/library/constructions/projection.cpp | 8 ++------
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 98ff4ae6cc..aa12a26b5d 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -421,13 +421,13 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
   pure { name := view.ctor.declName, type := type }
 
 @[extern "lean_mk_projections"]
-private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except String Environment
+private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except KernelException Environment
 
 private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : TermElabM Unit := do
   let env ← getEnv
   match mkProjections env structName projs isClass with
-  | Except.ok env    => setEnv env
-  | Except.error msg => throwError msg
+  | Except.ok env   => setEnv env
+  | Except.error ex => throwKernelException ex
 
 private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
   let env ← getEnv
diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp
index 4d1e9f5f46..850ba28f9b 100644
--- a/src/library/constructions/projection.cpp
+++ b/src/library/constructions/projection.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <lean/sstream.h>
+#include "kernel/kernel_exception.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive.h"
@@ -121,12 +122,7 @@ extern "C" object * lean_mk_projections(object * env, object * struct_name, obje
         bool infer_mod = cnstr_get_uint8(p.raw(), sizeof(object*));
         infer_kinds.push_back(infer_mod ? implicit_infer_kind::Implicit : implicit_infer_kind::RelaxedImplicit);
     }
-    try {
-        new_env = mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0);
-        return mk_except_ok(new_env);
-    } catch (exception & ex) {
-        return mk_except_error(string_ref(ex.what()));
-    }
+    return catch_kernel_exceptions<environment>([&]() { return mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0); });
 }
 
 void initialize_def_projection() {