diff options
Diffstat (limited to 'lib/dyn.ml')
-rw-r--r-- | lib/dyn.ml | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/lib/dyn.ml b/lib/dyn.ml new file mode 100644 index 00000000..63f00365 --- /dev/null +++ b/lib/dyn.ml @@ -0,0 +1,27 @@ +(************************************************************************) +(* 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: dyn.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *) + +open Util + +(* Dynamics, programmed with DANGER !!! *) + +type t = string * Obj.t + +let dyntab = ref ([] : string list) + +let create s = + if List.mem s !dyntab then + anomaly ("Dyn.create: already declared dynamic " ^ s); + dyntab := s :: !dyntab; + ((fun v -> (s,Obj.repr v)), + (fun (s',rv) -> + if s = s' then Obj.magic rv else failwith "dyn_out")) + +let tag (s,_) = s |