diff options
| author | letouzey | 2002-12-03 16:04:21 +0000 |
|---|---|---|
| committer | letouzey | 2002-12-03 16:04:21 +0000 |
| commit | 436ed028434916e58f697593834cbfcc220f8c13 (patch) | |
| tree | 5d2b58e2e91564203ab27229645367ba1666c31c /contrib/interface | |
| parent | 80b8609c3b3aca8ac5b8af145b12956a41ab78f9 (diff) | |
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 2 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index ded82a6916..fd8d64f07d 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -414,7 +414,7 @@ let inspect n = (sp,_), "VARIABLE" -> let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v - | (sp,kn), ("CONSTANT"|"PARAMETER") -> + | (sp,kn), "CONSTANT" -> let {const_type=typ} = Global.lookup_constant kn in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index a7e1f34449..80009d7838 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -205,7 +205,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = let tag = object_tag lobj in match tag with | "VARIABLE" -> variable_to_ast_list (basename sp) - | "CONSTANT"|"PARAMETER" -> constant_to_ast_list kn + | "CONSTANT" -> constant_to_ast_list kn | "INDUCTIVE" -> inductive_to_ast_list kn | s -> errorlabstrm |