Nettoyage des fichiers de parsing

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

1 files changed, 7 insertions, 15 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index e62e85d57d..1d20f928a3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -28,21 +28,11 @@ let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
 (* 1| Constant definitions *)
 
-let constant_entry_of_com com =
+let constant_entry_of_com (com,comtypopt) =
   let sigma = Evd.empty in
   let env = Global.env() in
-  match com with
-    | Node(_,"CAST",[_;t]) ->
-        { const_entry_body = Cooked (constr_of_com sigma env com);
-	  const_entry_type = Some (constr_of_com1 true sigma env t) }
-    | _ -> 
-	{ const_entry_body = Cooked (constr_of_com sigma env com);
-	  const_entry_type = None }
-
-let definition_body ident n com = 
-  let ce = constant_entry_of_com com in
-  declare_constant ident (ce,n);
-  if is_verbose() then message ((string_of_id ident) ^ " is defined")
+    { const_entry_body = Cooked (constr_of_com sigma env com);
+      const_entry_type = option_app (constr_of_com1 true sigma env) comtypopt }
 
 let red_constant_entry ce = function
   | None -> ce
@@ -56,12 +46,14 @@ let red_constant_entry ce = function
 	const_entry_type = 
 	  ce.const_entry_type }
 
-let definition_body_red ident n com red_option = 
-  let ce = constant_entry_of_com com in
+let definition_body_red ident n com comtypeopt red_option = 
+  let ce = constant_entry_of_com (com,comtypeopt) in
   let ce' = red_constant_entry ce red_option in
   declare_constant ident (ce',n);
   if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
+let definition_body ident n com typ = definition_body_red ident n com typ None
+
 let syntax_definition ident com =
   let c = raw_constr_of_com Evd.empty (Global.context()) com in 
   Syntax_def.declare_syntactic_definition ident c;