From d050094c578bdf5fc0611b808949fee28ae2a641 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 26 Oct 2019 01:13:24 +0200
Subject: [proof] Remove duplication in the proof save path.

We move towards more unification in the proof save path of interactive
and non-interactive proofs.
---
 vernac/declareDef.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1bb6620886..786169f409 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,6 +44,7 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
+  -> ?should_suggest:bool
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
@@ -62,6 +63,16 @@ val declare_fix
   -> Impargs.manual_implicits
   -> GlobRef.t
 
+val declare_assumption
+  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> name:Id.t
+  -> scope:locality
+  -> hook:Hook.t option
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Entries.parameter_entry
+  -> GlobRef.t
+
 val prepare_definition
   :  allow_evars:bool
   -> ?opaque:bool
-- 
cgit v1.2.3


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.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 786169f409..17c2862cad 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,7 +44,6 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> ?should_suggest:bool
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
-- 
cgit v1.2.3


From b35dae7a6a9cc08c4bcdce7409e0ef45382b7ee1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 00:46:23 -0500
Subject: [declare] Remove trivial wrapper

In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.

Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...
---
 vernac/declareDef.mli | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 17c2862cad..c668ab2ac4 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -49,19 +49,6 @@ val declare_definition
   -> Impargs.manual_implicits
   -> GlobRef.t
 
-val declare_fix
-  :  ?opaque:bool
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> name:Id.t
-  -> scope:locality
-  -> kind:Decls.definition_object_kind
-  -> UnivNames.universe_binders
-  -> Entries.universes_entry
-  -> Evd.side_effects Entries.proof_output
-  -> Constr.types
-  -> Impargs.manual_implicits
-  -> GlobRef.t
-
 val declare_assumption
   :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> name:Id.t
-- 
cgit v1.2.3