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

2 files changed, 4 insertions, 10 deletions

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