diff options
Diffstat (limited to 'lib/stamps.ml')
| -rw-r--r-- | lib/stamps.ml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/lib/stamps.ml b/lib/stamps.ml new file mode 100644 index 00000000..1697c309 --- /dev/null +++ b/lib/stamps.ml @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: stamps.ml,v 1.2.16.1 2004/07/16 19:30:31 herbelin Exp $ *) + +let new_stamp = + let stamp_ctr = ref 0 in + fun () -> incr stamp_ctr; !stamp_ctr + +type 'a timestamped = { stamp : int; ed : 'a } + +let ts_stamp st = st.stamp +let ts_mod f st = { stamp = new_stamp(); ed = f st.ed } +let ts_it st = st.ed +let ts_mk v = { stamp = new_stamp(); ed = v} +let ts_eq st1 st2 = st1.stamp = st2.stamp + +type 'a idstamped = 'a timestamped + +let ids_mod f st = { stamp = st.stamp; ed = f st.ed} +let ids_it = ts_it +let ids_mk = ts_mk +let ids_eq = ts_eq |