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]
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial/tuto1/src')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 2fdca15552..3b906324f4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+  let sigma, ce = DeclareDef.prepare_definition
       ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubind = Evd.universe_binders sigma in
-- 
cgit v1.2.3