aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/unshare.mli
blob: 31ba90372ebb7af8a1a7469a5e3085b3018f39c1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
(*         *   University of Bologna                                    *)
(************************************************************************)
(*          This file is distributed under the terms of the             *)
(*           GNU Lesser General Public License Version 2.1              *)
(*                                                                      *)
(*                 Copyright (C) 2000-2004, HELM Team.                  *)
(*                       http://helm.cs.unibo.it                        *)
(************************************************************************)

exception CanNotUnshare;;

(* [unshare t] gives back a copy of t where all sharing has been removed   *)
(* Physical equality becomes meaningful on unshared terms. Hashtables that *)
(* use physical equality can now be used to associate information to evey  *)
(* node of the term.                                                       *)
val unshare: ?already_unshared:('a -> bool) -> 'a -> 'a