From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Mar 2020 03:07:42 -0400
Subject: [declare] [obligations] Refactor preparation of obligation entry

Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.

This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:

- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
---
 vernac/comProgramFixpoint.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3bac0419ef..f20b294499 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = DeclareDef.Hook.make (hook sigma) in
-  Obligations.check_evars env sigma;
+  RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 def typ
+    RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
@@ -287,7 +287,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
-      Obligations.eterm_obligations env id evm
+      RetrieveObl.retrieve_obligations env id evm
         (List.length rec_sign) def typ in
     (id, def, typ, imps, evars)
   in
-- 
cgit v1.2.3


From f836b601e3cb81dd24d25ccd910b2506aac998d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 17:08:16 -0400
Subject: [program] Use common type for fixpoint declarations.

---
 vernac/comProgramFixpoint.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index f20b294499..56780d00a6 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -281,15 +281,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
     (* Solve remaining evars *)
   let evd = nf_evar_map_undefined evd in
-  let collect_evars id def typ imps =
+  let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
-      RetrieveObl.retrieve_obligations env id evm
+      RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    (id, def, typ, imps, evars)
+    ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
-- 
cgit v1.2.3