summaryrefslogtreecommitdiff
path: root/library/libobject.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /library/libobject.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'library/libobject.ml')
-rw-r--r--library/libobject.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/libobject.ml b/library/libobject.ml
index 7f383a3b..709fb1bb 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: libobject.ml 9104 2006-09-01 11:04:44Z notin $ *)
open Util
open Names
@@ -144,7 +144,7 @@ let apply_dyn_fun deflt f lobj =
else
anomaly
("Cannot find library functions for an object with tag "^tag) in
- f dodecl
+ f dodecl
with
Failure "local to_apply_dyn_fun" -> deflt;;