From 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 29 Feb 2020 15:25:42 -0500
Subject: [lemmas] Handle mutual lemmas more uniformly.

We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.

This should be almost semantically equivalent to the previous code,
including some questionable choices present there.

In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
---
 vernac/declareDef.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index bd857a6e38..dea2ccb9af 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,8 +43,10 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data ?(should_suggest=false) udecl ce imps =
+let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Declare.Internal.get_fix_exn ce in
+  let should_suggest = ce.Declare.proof_entry_opaque &&
+                       Option.is_empty ce.Declare.proof_entry_secctx in
   let dref = match scope with
   | Discharge ->
     let () = declare_variable ~name ~kind (SectionLocalDef ce) in
-- 
cgit v1.2.3