From f17fa1daa613a4f86e6bdbf51ed7e758f158f938 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Feb 2015 16:25:20 +0100
Subject: STM: proof state also includes meta counters

Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
---
 pretyping/evarutil.ml  | 8 ++++++--
 pretyping/evarutil.mli | 3 +++
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0b8cbff36c..201a16ebeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 92a3984ba6..49036798e6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -243,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
-- 
cgit v1.2.3