diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /library | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 10 | ||||
| -rw-r--r-- | library/declare.mli | 2 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/goptions.mli | 2 | ||||
| -rw-r--r-- | library/impargs.mli | 2 | ||||
| -rw-r--r-- | library/indrec.mli | 2 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | library/libobject.mli | 2 | ||||
| -rw-r--r-- | library/library.mli | 2 | ||||
| -rwxr-xr-x | library/nametab.mli | 2 | ||||
| -rw-r--r-- | library/states.ml | 3 | ||||
| -rw-r--r-- | library/states.mli | 2 | ||||
| -rw-r--r-- | library/summary.mli | 2 |
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 |