From e2e4912212c5f6ab94eaded61e53b0478f9b17c8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 7 Mar 2020 04:25:40 -0500
Subject: [obligations] More progress towards unification of the save path

We make internal types `private` as an step towards the unification of
the save path with the rest of the system.

In particular, this is allow us to guarantee invariants
w.r.t. external users as the large majority of fields are always
constant.

This will also enable at some point a common creation of proof entry
with the rest of the system.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 73356c42f1..62556d38ff 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
     Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+    DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
 
   type partial_state =
     [ `Full of Vernacstate.t
-- 
cgit v1.2.3