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/declare.ml | |
| 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/declare.ml')
| -rw-r--r-- | library/declare.ml | 10 |
1 files changed, 10 insertions, 0 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 = |