Nettoyage des fichiers de parsing

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

3 files changed, 20 insertions, 26 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;
diff --git a/toplevel/command.mli b/toplevel/command.mli
index eaeb289c09..cd4cb930d5 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -10,10 +10,11 @@ open Declare
 (* Declaration functions. The following functions take ASTs, transform them
    into [constr] and then call the corresponding functions of [Declare]. *)
 
-val definition_body : identifier -> strength -> Coqast.t -> unit
+val definition_body : identifier -> strength -> 
+  Coqast.t -> Coqast.t option -> unit
 
-val definition_body_red : identifier -> strength -> Coqast.t 
-  -> Tacred.red_expr option -> unit
+val definition_body_red : identifier -> strength ->
+  Coqast.t -> Coqast.t option -> Tacred.red_expr option -> unit
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 54629fe2d3..e69d537a1a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -724,13 +724,14 @@ let _ =
 let _ =
   add "DEFINITION"
     (function 
-       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c ::optred) ->
-	   let red_option = match optred with 
-	     | [] -> None
-	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] -> 
-		 let env = Global.env() in
-		 let redexp = redexp_of_ast Evd.empty env (r1,r2) in 
-		 Some redexp
+       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c :: rest) ->
+	   let typ_opt,red_option = match rest with
+	     | [] -> None, None
+	     | [VARG_CONSTR t] -> Some t, None
+	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] ->
+		 None, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
+	     | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp(r1,r2))] ->
+		 Some t, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
 	     | _ -> bad_vernac_args "DEFINITION"
 	   in 
 	   let stre,coe,objdef,idcoe = match kind with
@@ -748,7 +749,7 @@ let _ =
              | _       -> anomaly "Unexpected string"
 	   in 
 	   fun () ->
-	     definition_body_red id stre c red_option;
+	     definition_body_red id stre c typ_opt red_option;
              if coe then begin
 	       Class.try_add_new_coercion id stre;
                message ((string_of_id id) ^ " is now a coercion")