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/comFixpoint.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b6843eab33..a29d60ccde 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,8 +255,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
     | None -> Decls.CoFixpoint, true, []
   in
   let thms =
-    List.map3 (fun name t (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ = EConstr.of_constr t
+    List.map3 (fun name typ (ctx,impargs,_) ->
+        { Lemmas.Recthm.name; typ
         ; args = List.map RelDecl.get_name ctx; impargs})
       fixnames fixtypes fiximps in
   let init_tac =
-- 
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/comFixpoint.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a29d60ccde..65dffb3c0b 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Decls.Fixpoint
-    | None -> [], true, Decls.CoFixpoint
+    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
+    | None -> [], true, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
@@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
-  let pl = Evd.universe_binders evd in
-  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
-  let fixdecls = List.map mk_pure fixdecls in
-  ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx)
-            fixnames fixdecls fixtypes fiximps);
+  let udecl = Evd.universe_binders evd in
+  let _ : GlobRef.t list =
+    List.map4 (fun name body types imps ->
+        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
+        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+      fixnames fixdecls fixtypes fiximps
+  in
   recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
-- 
cgit v1.2.3