diff options
| author | filliatr | 1999-11-26 13:52:34 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-26 13:52:34 +0000 |
| commit | 3d4a8fc16cf415643be2a5707248c1858a307023 (patch) | |
| tree | 0fa6315a2d48ef5f7a78b808cddc14feeb90763c /library | |
| parent | ba86510ae228cd70dd88719453ba8f5c07250682 (diff) | |
prvecti
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@151 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index aca22ebd2c..52355a7e28 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -38,7 +38,7 @@ let (in_variable, out_variable) = load_function = load_variable; open_function = open_variable; specification_function = specification_variable } in - declare_object ("Variable", od) + declare_object ("VARIABLE", od) let declare_variable id c = let obj = (id,c) in @@ -63,7 +63,7 @@ let (in_parameter, out_parameter) = load_function = (fun _ -> ()); open_function = open_parameter; specification_function = specification_parameter } in - declare_object ("Parameter", od) + declare_object ("PARAMETER", od) let declare_parameter id c = let sp = add_leaf id CCI (in_parameter c) in @@ -89,7 +89,7 @@ let (in_constant, out_constant) = load_function = (fun _ -> ()); open_function = open_constant; specification_function = specification_constant } in - declare_object ("Constant", od) + declare_object ("CONSTANT", od) let declare_constant id ce = let sp = add_leaf id CCI (in_constant ce) in @@ -123,7 +123,7 @@ let (in_inductive, out_inductive) = load_function = (fun _ -> ()); open_function = open_inductive; specification_function = specification_inductive } in - declare_object ("Inductive", od) + declare_object ("INDUCTIVE", od) let declare_mind mie = let id = match mie.mind_entry_inds with |