Réorganisation de la structure interne des types de déclarations (decl_kinds)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 4 insertions, 19 deletions

diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 50c8a0fa1a..b06ba1992d 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -140,7 +140,7 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition ((Global,Definition false), (dummy_loc,name), DefineBody ([], None,
+  VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ea7b521624..f17cb67b43 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1361,24 +1361,9 @@ let coerce_genarg_to_VARG x =
   | ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
 
 
-let xlate_thm x = CT_thm (match x with
-  | Theorem -> "Theorem"
-  | Remark -> "Remark"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact")
-
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition _) -> "Local"
- | (Global, Definition true) -> "Boxed Definition"
- | (Global, Definition false) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) -> 
-     xlate_error "Local CanonicalStructure not parsed")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
+
+let xlate_defn k = CT_defn (string_of_definition_kind k)
 
 let xlate_var x = CT_var (match x with
  | (Global,Definitional) -> "Parameter"