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

5 files changed, 7 insertions, 13 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 811591bd8..5d82bad51 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -106,7 +106,7 @@ let extract_module m =
   let get_reference = function
     | (_,kn), Leaf o ->
 	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
+	   | "CONSTANT" -> ConstRef kn
 	   | "INDUCTIVE" -> IndRef (kn,0)
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index ded82a691..fd8d64f07 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 a7e1f3444..80009d783 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 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 07df70a0c..b05b7baa8 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -32,8 +32,7 @@ exception Uninteresting;;
 (*CSC: CODE USEFUL ONLY FOR THE CODE COMMENTED OUT
 let tag_of_string_tag =
  function
-    "CONSTANT"
-  | "PARAMETER"       -> Constant
+    "CONSTANT"        -> Constant
   | "INDUCTIVE"       -> Inductive
   | "VARIABLE"        -> Variable
   | _                 -> raise Uninteresting
@@ -76,7 +75,6 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
           | DK.Local  -> false (* a local definition *)
           | DK.Global -> true  (* a non-local one    *)
         )
-    | "PARAMETER"                 (* axioms and                               *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
     | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
@@ -541,8 +539,7 @@ let print_coq_object lobj id sp dn fv env =
     let tag = tag_of_string_tag strtag in
     let obj =
      match strtag with
-        "CONSTANT"  (* = Definition, Theorem *)
-      | "PARAMETER" (* = Axiom *) ->
+        "CONSTANT"  (* = Definition, Theorem, Axiom *)
           let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
            G.lookup_constant sp
           in
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 5ca89dd3f..3aaf77615 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -38,8 +38,7 @@ exception Uninteresting;;
 
 let tag_of_string_tag =
  function
-    "CONSTANT"
-  | "PARAMETER"       -> Constant
+    "CONSTANT"        -> Constant
   | "INDUCTIVE"       -> Inductive
   | "VARIABLE"        -> Variable
   | _                 -> raise Uninteresting
@@ -89,7 +88,6 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
           | L.NotDeclare     -> false (* not a definition *)
           | L.NeverDischarge -> true  (* a non-local one    *)
         )
-    | "PARAMETER"                 (* axioms and                               *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
     | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
@@ -848,8 +846,7 @@ let print_object lobj id (sp,kn) dn fv env =
     let inner_types = ref [] in
     let pp_cmds =
      match strtag with
-        "CONSTANT"  (* = Definition, Theorem *)
-      | "PARAMETER" (* = Axiom *) ->
+        "CONSTANT" -> (* = Definition, Theorem, Axiom *)
           let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
            G.lookup_constant kn
           in