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