aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml10
-rw-r--r--library/declare.mli2
-rw-r--r--library/global.mli2
-rw-r--r--library/goptions.mli2
-rw-r--r--library/impargs.mli2
-rw-r--r--library/indrec.mli2
-rw-r--r--library/lib.mli2
-rw-r--r--library/libobject.mli2
-rw-r--r--library/library.mli2
-rwxr-xr-xlibrary/nametab.mli2
-rw-r--r--library/states.ml3
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.mli2
13 files changed, 22 insertions, 13 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 127f60b66..305dd815b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -153,7 +153,16 @@ let (in_constant, out_constant) =
in
declare_object ("CONSTANT", od)
+let hcons_constant_declaration = function
+ | (ConstantEntry ce, stre) ->
+ (ConstantEntry
+ { const_entry_body = hcons1_constr ce.const_entry_body;
+ const_entry_type = option_app hcons1_constr ce.const_entry_type },
+ stre)
+ | cd -> cd
+
let declare_constant id cd =
+ (* let cd = hcons_constant_declaration cd in *)
let sp = add_leaf id CCI (in_constant cd) in
if is_implicit_args() then declare_constant_implicits sp
@@ -228,6 +237,7 @@ let declare_mind mie =
if is_implicit_args() then declare_mib_implicits sp;
sp
+
(*s Test and access functions. *)
let is_constant sp =
diff --git a/library/declare.mli b/library/declare.mli
index 38a14c010..5f9f8ba36 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/global.mli b/library/global.mli
index 05af78a01..0ad3e3713 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/goptions.mli b/library/goptions.mli
index 3cdc122e5..08f5262eb 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* This module manages customization parameters at the vernacular level *)
diff --git a/library/impargs.mli b/library/impargs.mli
index e97a0a41e..bc52caea0 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/indrec.mli b/library/indrec.mli
index 728b3c5dc..8a47c1fae 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/lib.mli b/library/lib.mli
index ed08bcc1d..bc4032a61 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/libobject.mli b/library/libobject.mli
index 17a221a66..7b63af380 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/library.mli b/library/library.mli
index 4d4a2d19b..2f9ee2500 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/nametab.mli b/library/nametab.mli
index 7382b447d..13c6b514b 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/library/states.ml b/library/states.ml
index b5c45383d..5a4983a80 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,8 +12,7 @@ let get_state () =
let set_state (fl,fs) =
Lib.unfreeze fl;
- unfreeze_summaries fs;
- Lib.declare_initial_state()
+ unfreeze_summaries fs
let state_magic_number = 19764
diff --git a/library/states.mli b/library/states.mli
index 46cc2f68d..5ff97d103 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*s States of the system. In that module, we provide functions to get
and set the state of the whole system. Internally, it is done by
diff --git a/library/summary.mli b/library/summary.mli
index fc639d7f8..feca53fe3 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names