diff options
author | 2001-09-18 17:20:22 +0000 | |
---|---|---|
committer | 2001-09-18 17:20:22 +0000 | |
commit | e566468b8630116f7c9fa5499ae72aa5aa38b2d9 (patch) | |
tree | 451333328afdfc0f144be20f2799d73c5da259b4 /library/lib.ml | |
parent | f494f444ca06a573713aede990ba93a58ea4cf13 (diff) |
Mise en place de noms contenant la section pour Fact et Remark
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index 5995a9600..94cba5e0c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -95,6 +95,10 @@ let add_anonymous_entry node = add_entry sp node; sp +let add_absolutely_named_lead sp obj = + cache_object (sp,obj); + add_entry sp (Leaf obj) + let add_leaf id kind obj = let sp = make_path id kind in cache_object (sp,obj); |