diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-11-17 12:44:14 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-11-17 12:44:14 -0500 |
| commit | ed279aaf89fd1d8b92b26adba6b3e8e34b88c254 (patch) | |
| tree | 9e63f1f3850a9309718b5c95fde780c56c801325 /src/disjoint.sml | |
| parent | 381f4d4ab67b2c76cbd89470eb2a5ddd407965d5 (diff) | |
Hooks for measuring how much interesting proving is going on in elaboration
Diffstat (limited to 'src/disjoint.sml')
| -rw-r--r-- | src/disjoint.sml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |