From 8030a420d2cfcf8372d5fe6544efbecde940381b Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 12 Dec 2000 22:07:41 +0000
Subject: syntaxe AST Inversion + commentaires ocamlweb autour de $

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml    | 10 ++++++++++
 library/declare.mli   |  2 +-
 library/global.mli    |  2 +-
 library/goptions.mli  |  2 +-
 library/impargs.mli   |  2 +-
 library/indrec.mli    |  2 +-
 library/lib.mli       |  2 +-
 library/libobject.mli |  2 +-
 library/library.mli   |  2 +-
 library/nametab.mli   |  2 +-
 library/states.ml     |  3 +--
 library/states.mli    |  2 +-
 library/summary.mli   |  2 +-
 13 files changed, 22 insertions(+), 13 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3