From 1320d5004b58f33c2274bfdc0629d7f513cd49c4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 30 Mar 2020 15:02:50 -0400
Subject: [declare] [nit] Get `fix_exn` only in the case of an exception.

Suggested by Gaëtan Gilbert.
---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 356e8f091e..1607771598 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -60,10 +60,10 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
   dref
 
 let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry =
-  let fix_exn = Declare.Internal.get_fix_exn entry in
   try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry
   with exn ->
     let exn = Exninfo.capture exn in
+    let fix_exn = Declare.Internal.get_fix_exn entry in
     Exninfo.iraise (fix_exn exn)
 
 let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
-- 
cgit v1.2.3