aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-03-22 11:07:58 +0100
committerGaëtan Gilbert2020-03-22 11:07:58 +0100
commit7ba059507b67b1f6ea3566a5d1dee40f6af78316 (patch)
treecb901254b587eabdb2c508fdf60a9bbc23971920 /stm
parentb048ecb6d874e1eb2e33c1fa3a15d3a508500285 (diff)
parentc3350ed82e1dd4e299a5a14e6e63103556a379d2 (diff)
Merge PR #11731: [proof] Miscellaneous refactorings
Reviewed-by: SkySkimmer Reviewed-by: gares
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
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