From 4bc02a044fde4fb5c6f347e942202307a2dbdaaa Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 17 Nov 2009 12:44:14 -0500
Subject: Hooks for measuring how much interesting proving is going on in
 elaboration

---
 src/disjoint.sml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/disjoint.sml')

diff --git a/src/disjoint.sml b/src/disjoint.sml
index 5cc9d1fb..8fa8834c 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -161,6 +161,10 @@ fun prove1 denv (p1, p2) =
             NONE => false
           | SOME pset => PS.member (pset, p2)
 
+val proved = ref 0
+fun reset () = (ElabOps.reset ();
+                proved := 0)
+
 fun decomposeRow env c =
     let
         val loc = #2 c
@@ -248,6 +252,7 @@ and assert env denv (c1, c2) =
 
 and prove env denv (c1, c2, loc) =
     let
+        val () = proved := !proved + 1
         val ps1 = decomposeRow env c1
         val ps2 = decomposeRow env c2
 
-- 
cgit v1.2.3