Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour

les définitions


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

11 files changed, 155 insertions, 122 deletions

diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 5ba5e0e7e8..8c6293ae2c 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -161,9 +161,9 @@ let make_definition_ast name c typ implicits =
   (implicits_to_ast_list implicits);;
 *)
 let make_definition_ast name c typ implicits =
-  VernacDefinition (Definition, name, None,
-    (ope("CAST", [(constr_to_ast c);(constr_to_ast (body_of_type typ))])),
-    None, (fun _ _ -> ()))
+  VernacDefinition (Definition, name, DefineBody ([], None,
+    (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
+    (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
 (* This function is inspired by print_constant *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 233af4f7d0..d1af58df70 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2582,7 +2582,7 @@ let xlate_vernac =
      | "FOCUS", [Varg_int n] -> CT_focus (CT_coerce_INT_to_INT_OPT n)
      | "UNFOCUS", [] -> CT_unfocus
 *)
-    | VernacStartProof (_, None, c, _, _) ->
+    | VernacGoal c ->
 	CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_constr c))
     | VernacAbort (Some id) -> CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id))
     | VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
@@ -2869,9 +2869,9 @@ let xlate_vernac =
      | "StartProof",
          ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) ->
 *)
-  | VernacStartProof (kind, Some s, c, _, _) ->
+  | VernacStartTheoremProof (k, s, c, _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
-	CT_theorem_goal (xlate_defn_or_thm kind, xlate_ident s,xlate_constr c))
+	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_constr c))
 (*
      | (*My attempt: suspend and resume as separate nodes *)
        "SUSPEND", [] -> CT_suspend
@@ -2898,7 +2898,12 @@ let xlate_vernac =
                     (CT_coerce_SORT_TYPE_to_FORMULA b), None
 	   | _ -> assert false in
 *)
-  | VernacDefinition (kind,s,red_option,c,typ_opt,_) ->
+  | VernacDefinition (k,s,ProveBody (bl,typ),_) ->
+      if bl <> [] then xlate_error "TODO: Def bindings";
+      CT_coerce_THEOREM_GOAL_to_COMMAND(
+	CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_constr typ))
+  | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_) ->
+      if bl <> [] then xlate_error "TODO: Def bindings";
       CT_definition
 	(xlate_defn kind, xlate_ident s, 
 	   cvt_optional_eval_for_definition c red_option,
diff --git a/parsing/ast.ml b/parsing/ast.ml
index 1a4be70d9d..e1d885a221 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -264,6 +264,11 @@ let abstract_binders_ast loc name a b =
 	List.fold_right (abstract_binder_ast loc name) l b
     | _ -> invalid_arg "Bad usage of $ABSTRACT macro"
 
+let mkCastC(a,b) = ope("CAST",[a;b])
+let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
+let mkLetInC(x,a,b) = ope("LETIN",[a;slam(Some x,b)])
+let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
+
 (* Pattern-matching on ast *)
 
 let env_assoc_value loc v env =
diff --git a/parsing/ast.mli b/parsing/ast.mli
index fd7581199f..4a9048256d 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -107,6 +107,11 @@ val coerce_reference_to_id : Tacexpr.reference_expr -> identifier
 val abstract_binders_ast :
   Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t
 
+val mkCastC : Coqast.t * Coqast.t -> Coqast.t
+val mkLambdaC : identifier * Coqast.t * Coqast.t -> Coqast.t
+val mkLetInC : identifier * Coqast.t * Coqast.t -> Coqast.t
+val mkProdC : identifier * Coqast.t * Coqast.t -> Coqast.t
+
 exception No_match of string
 
 val isMeta : string -> bool
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9f5ef5c8be..d4a00346b7 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -33,8 +33,7 @@ GEXTEND Gram
     | ":"; l = LIST1 IDENT -> l ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = Constr.constr -> 
-        VernacStartProof(StartTheoremProof Theorem,None,c,false,(fun _ _ ->()))
+    [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
 (*VernacGoal c*)
 (*      | IDENT "Goal" -> VernacGoal None*)
       | "Proof" -> VernacNop
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 86e7629aa8..16af5ea976 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -25,26 +25,13 @@ let join_binders (idl,c) = List.map (fun id -> (id,c)) idl
 
 open Genarg
 
-let cast_constr loc c = function
-  | None -> c
-  | Some t -> <:ast< (CAST $c $t) >>
-
-let abstract_constr bl c =
-  let loc = dummy_loc in 
-  <:ast<($ABSTRACT "LAMBDALIST" $bl $c)>>
-
-let generalize_constr bl c =
-  let loc = dummy_loc in 
-  <:ast< ($ABSTRACT "PRODLIST" $bl $c) >>
-
-let evar_constr = let loc = dummy_loc in <:ast< (ISEVAR) >>
-
+let evar_constr loc = <:ast< (ISEVAR) >>
 
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
 GEXTEND Gram
-  GLOBAL: vernac;
+  GLOBAL: vernac gallina_ext;
   vernac:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
@@ -72,13 +59,10 @@ GEXTEND Gram
 	  VernacSolveExistential (n,c)
     ] ]
   ;
-  def_body:
-    [ [ ":="; c = constr; ":"; t = constr -> c, Some t
-      | ":"; t = constr; ":="; c = constr -> c, Some t
-      | ":="; c = constr -> c, None ] ]
-  ;
   constr_body:
-    [ [	(c,t) = def_body -> cast_constr loc c t ] ]
+    [ [ ":="; c = constr; ":"; t = constr -> <:ast< (CAST $c $t) >>
+      | ":"; t = constr; ":="; c = constr -> <:ast< (CAST $c $t) >>
+      | ":="; c = constr -> c ] ]
   ;
   vernac_list_tail:
     [ [ v = located_vernac; l = vernac_list_tail -> v :: l
@@ -111,8 +95,7 @@ GEXTEND Gram
       | IDENT "Local" -> (fun _ _ -> ()), LocalDefinition
       | IDENT "SubClass"  -> Class.add_subclass_hook, Definition
       | IDENT "Local"; IDENT "SubClass"  ->
-	  Class.add_subclass_hook, LocalDefinition
- ] ]  
+	  Class.add_subclass_hook, LocalDefinition ] ]  
   ;
   assumption_token:
     [ [ "Hypothesis" -> AssumptionHypothesis
@@ -138,38 +121,50 @@ GEXTEND Gram
   ne_params_list:
     [ [ ll = LIST1 params SEP ";" -> List.flatten ll ] ]
   ;
+ident_comma_list_tail:
+    [ [ ","; idl = LIST1 ident SEP "," -> idl | -> [] ] ]
+  ;
+  type_option:
+    [ [ ":"; c = constr -> c 
+      | -> evar_constr loc ] ]
+  ;
+  opt_casted_constr:
+    [ [ c = constr;  ":"; t = constr -> <:ast< (CAST $c $t) >>
+      | c = constr -> c ] ]
+  ;
+  vardecls:
+    [ [ id = ident; idl = ident_comma_list_tail; c = type_option ->
+          LocalRawAssum (id::idl,c)
+      | id = ident; [ "=" | ":=" ]; c = opt_casted_constr ->
+          LocalRawDef (id,c)
+    ] ]
+  ;
+  binders:
+    [ [ "["; bl = LIST1 vardecls SEP ";"; "]" -> bl ] ]
+  ;
+  binders_list:
+    [ [ bls = LIST0 binders -> List.flatten bls ] ]
+  ;
   reduce:
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
       | -> None ] ]
   ;
-  binders_list:
-    [ [ idl = ne_binders_list -> <:ast< (BINDERS ($LIST $idl)) >>
-      | -> <:ast< (BINDERS) >> ] ]
+  def_body:
+    [ [ bl = binders_list; ":="; red = reduce; c = constr; ":"; t = constr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = binders_list; ":"; t = constr; ":="; red = reduce; c = constr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = binders_list; ":="; red = reduce; c = constr ->
+          DefineBody (bl, red, c, None)
+      | bl = binders_list; ":"; t = constr ->
+          ProveBody (bl, t) ] ]
   ;
   gallina:
-    (* Definition, Goal *)
+    (* Definition, Theorem, Variable, Axiom, ... *)
     [ [ thm = thm_token; id = ident; ":"; c = constr -> 
-         VernacStartProof
-           (StartTheoremProof thm, Some id, c, false, (fun _ _ -> ()))
-
-      | (f,d) = def_token; id = ident; bl = binders_list;
-	":"; t = constr -> 
-          VernacStartProof 
-            (StartDefinitionBody d, Some id, generalize_constr bl t, false, f)
-      | (f,def) = def_token; s = Prim.ident; bl = binders_list;
-	":="; red = reduce; c = constr ->
-	  VernacDefinition
-	    (def, s, red, abstract_constr bl c, None, f)
-      | (f,def) = def_token; s = Prim.ident; bl = binders_list;
-	":="; red = reduce; c = constr; ":"; t = constr -> 
-	  VernacDefinition
-	    (def, s, red, abstract_constr bl c,
-            Some (generalize_constr bl t), f)
-      | (f,def) = def_token; s = Prim.ident; bl = binders_list;
-	":"; t = constr; ":="; red = reduce; c = constr -> 
-	  VernacDefinition
-	    (def, s, red, abstract_constr bl c,
-            Some (generalize_constr bl t), f)
+         VernacStartTheoremProof (thm, id, c, false, (fun _ _ -> ()))
+      | (f,d) = def_token; id = ident; b = def_body -> 
+          VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = ne_params_list -> 
 	  VernacAssumption (stre, bl)
       | stre = assumptions_token; bl = ne_params_list ->
@@ -177,12 +172,7 @@ GEXTEND Gram
 	  VernacAssumption (stre, bl)
       ] ]
   ;
-  END
-
-(* Gallina inductive declarations *)
-GEXTEND Gram
-  GLOBAL: gallina gallina_ext;
-
+  (* Gallina inductive declarations *)
   finite_token:
     [ [ "Inductive" -> true
       | "CoInductive" -> false ] ]
@@ -227,11 +217,6 @@ GEXTEND Gram
     [ [ ">" -> true
       |  -> false ] ]
   ;
-  of_type_with_opt_coercion:
-    [ [ ":>" -> true
-      | ":"; ">" -> true
-      | ":" -> false ] ]
-  ;
   onescheme:
     [ [ id = ident; ":="; dep = dep; ind = qualid; IDENT "Sort";
         s = sort -> (id,dep,ind,s) ] ]
@@ -271,7 +256,7 @@ GEXTEND Gram
   ;
   simple_params:
     [ [ idl = LIST1 ident SEP ","; ":"; c = constr -> join_binders (idl, c)
-      | idl = LIST1 ident SEP "," -> join_binders (idl, evar_constr)
+      | idl = LIST1 ident SEP "," -> join_binders (idl, evar_constr dummy_loc)
     ] ]
   ;
   simple_binders:
@@ -306,16 +291,6 @@ GEXTEND Gram
       | f = finite_token; indl = block ->
           VernacInductive (f,indl) ] ]
   ;
-  END
-
-GEXTEND Gram
-  GLOBAL: gallina_ext;
-
-  def_body:
-    [ [ ":="; c = constr; ":"; t = constr -> c, Some t
-      | ":"; t = constr; ":="; c = constr -> c, Some t
-      | ":="; c = constr -> c, None ] ]
-  ;
   gallina_ext:
     [ [ 
 (* Sections *)
@@ -332,20 +307,25 @@ GEXTEND Gram
 (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = qualid ->
 	  VernacCanonical qid
-      | IDENT "Canonical"; IDENT "Structure"; qid = qualid; (c,t) = def_body
-          ->
+      | IDENT "Canonical"; IDENT "Structure"; qid = qualid; d = def_body ->
           let s = Ast.coerce_qualid_to_id qid in
+	  VernacDefinition (Definition,s,d,Recordobj.add_object_hook)
+(*
 	  VernacDefinition (Definition,s,None,c,t,Recordobj.add_object_hook)
+*)
       (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
          (they were unused and undocumented) *)
 
 (* Coercions *)
-      | IDENT "Coercion"; qid = qualid; (c,t) = def_body ->
+      | IDENT "Coercion"; qid = qualid; d = def_body ->
           let s = Ast.coerce_qualid_to_id qid in
+(*
 	  VernacDefinition (Definition,s,None,c,t,Class.add_coercion_hook)
-      | IDENT "Coercion"; IDENT "Local"; qid = qualid; (c,t) = def_body ->
+*)
+	  VernacDefinition (Definition,s,d,Class.add_coercion_hook)
+      | IDENT "Coercion"; IDENT "Local"; qid = qualid; d = def_body ->
            let s = Ast.coerce_qualid_to_id qid in
-	  VernacDefinition (LocalDefinition,s,None,c,t,Class.add_coercion_hook)
+	  VernacDefinition (LocalDefinition,s,d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = Prim.ident;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Declare.make_strength_0 (), f, s, t)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 87ac8e3bac..80cdf953b9 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -369,7 +369,7 @@ and pr_atom1 = function
   | TacForward (true,na,c) ->
       hov 1 (str "Pose" ++ pr_name na ++ str ":=" ++ pr_constr c)
   | TacGeneralize l ->
-      hov 0 (str "Generalize" ++ brk (1,1) ++ prlist_with_sep spc pr_constr l)
+      hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l)
   | TacGeneralizeDep c ->
       hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
       pr_constr c)
@@ -417,18 +417,16 @@ and pr_atom1 = function
   | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id)
   | TacDestructConcl as x -> pr_atom0 x
   | TacSuperAuto (n,l,b1,b2) ->
-      hov 0 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
+      hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
              pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
   | TacDAuto (n,p) ->
-      hov 0 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
+      hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
 
   (* Context management *)
   | TacClear l ->
-      hov 0
-        (str "Clear" ++ brk (1,1) ++ prlist_with_sep spc (pr_metanum pr_id) l)
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
   | TacClearBody l ->
-      hov 0
-        (str "Clear" ++ brk (1,1) ++ prlist_with_sep spc (pr_metanum pr_id) l)
+      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l)
   | TacMove (b,(_,id1),(_,id2)) ->
       (* Rem: only b = true is available for users *)
       assert b;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c6a038c3b0..34adc05876 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,30 +33,44 @@ open Safe_typing
 open Nametab
 open Typeops
 open Indtypes
+open Vernacexpr
 
-let mkCastC(a,b) = ope("CAST",[a;b])
-let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
+let rec abstract_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC(x,t,b)) idl
+        (abstract_rawconstr c bl)
+
+let rec destSubCast c = match kind_of_term c with
+  | Lambda (x,t,c) -> 
+      let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
+  | LetIn (x,b,t,c) ->
+      let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
+  | Cast (b,u) -> (b,u)
+  | _ -> assert false
+
 (* Commands of the interface *)
 
 (* 1| Constant definitions *)
 
-let constant_entry_of_com (com,comtypopt,opacity) =
+let constant_entry_of_com (bl,com,comtypopt,opacity) =
   let sigma = Evd.empty in
   let env = Global.env() in
   match comtypopt with
       None -> 
-	{ const_entry_body = interp_constr sigma env com;
+	let b = abstract_rawconstr com bl in
+	{ const_entry_body = interp_constr sigma env b;
 	  const_entry_type = None;
           const_entry_opaque = opacity }
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = mkCastC (com,comtyp) in
-	let (body,typ) = destCast (interp_constr sigma env b) in
+	let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in
+	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity }
@@ -75,8 +89,10 @@ let declare_global_definition ident ce n local =
   if_verbose message ((string_of_id ident) ^ " is defined");
   ConstRef sp
 
-let declare_definition red_option ident (local,n) c typopt = 
-  let ce = constant_entry_of_com (c,typopt,false) in
+let declare_definition ident (local,n) bl red_option c typopt = 
+  let ce = constant_entry_of_com (bl,c,typopt,false) in
+  if bl<>[] && red_option <> None then 
+    error "Evaluation under a local context not supported";
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge -> declare_global_definition ident ce' n local
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ea6c97e0ea..1b8cbe49a1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Nametab
 open Library
+open Vernacexpr
 (*i*)
 
 (*s Declaration functions. The following functions take ASTs,
@@ -21,8 +22,9 @@ open Library
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
-val declare_definition : Tacred.red_expr option -> identifier
-  -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference
+val declare_definition : identifier -> bool * strength ->
+  local_binder list -> Tacred.red_expr option -> Coqast.t -> Coqast.t option
+    -> global_reference
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 68ab007559..3852ba7fe0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -267,15 +267,33 @@ let interp_goal = function
   | StartTheoremProof x -> (false, interp_theorem x)
   | StartDefinitionBody x -> interp_definition x
 
-let vernac_definition kind id red_option c typ_opt hook = 
-  let red_option = match red_option with
-    | None -> None 
-    | Some r -> 
-	let (evc,env)= Command.get_current_context () in
-	Some (interp_redexp env evc r) in
-  let (local,stre as x) = interp_definition kind in
-  let ref = declare_definition red_option id x c typ_opt in
-  hook stre ref
+let start_proof_and_print idopt k t hook =
+  start_proof_com idopt k t hook;
+  print_subgoals ();
+  if !pcoq <> None then (out_some !pcoq).start_proof ()
+
+let rec generalize_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (id,b)::bl -> Ast.mkLetInC(id,b,generalize_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> Ast.mkProdC(x,t,b)) idl
+        (generalize_rawconstr c bl)
+
+let vernac_definition kind id def hook =
+  let (local,stre as k) = interp_definition kind in
+  match def with
+  | ProveBody (bl,t) ->
+      let hook _ _ = () in
+      let t = generalize_rawconstr t bl in
+      start_proof_and_print (Some id) k t hook
+  | DefineBody (bl,red_option,c,typ_opt) ->
+      let red_option = match red_option with
+        | None -> None
+        | Some r -> 
+	    let (evc,env)= Command.get_current_context () in
+	    Some (interp_redexp env evc r) in
+      let ref = declare_definition id k bl red_option c typ_opt in
+      hook stre ref
 
 let vernac_start_proof kind sopt t lettop hook =
   if not(refining ()) then
@@ -284,9 +302,7 @@ let vernac_start_proof kind sopt t lettop hook =
 	(str "Let declarations can only be used in proof editing mode")
 (*    else if s = None then
       error "repeated Goal not permitted in refining mode"*);
-  start_proof_com sopt (interp_goal kind) t hook;
-  print_subgoals ();
-  if !pcoq <> None then (out_some !pcoq).start_proof ()
+  start_proof_and_print sopt (false, interp_theorem kind) t hook
 
 let vernac_end_proof is_opaque idopt =
   if_verbose show_script ();
@@ -866,8 +882,9 @@ let interp c = match c with
   | VernacDistfix (assoc,n,inf,qid) -> vernac_distfix assoc n inf qid
 
   (* Gallina *)
-  | VernacDefinition (k,id,red,t,otyp,f) -> vernac_definition k id red t otyp f
-  | VernacStartProof (k,id,t,top,f) -> vernac_start_proof k id t top f
+  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
+  | VernacStartTheoremProof (k,id,t,top,f) ->
+      vernac_start_proof k (Some id) t top f
   | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,l) -> vernac_assumption stre l
@@ -929,7 +946,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-(*  | VernacGoal c -> vernac_goal c*)
+  | VernacGoal t -> vernac_start_proof Theorem None t false (fun _ _ -> ())
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index f1bd6ed52d..ace11aee30 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -149,6 +149,13 @@ type fixpoint_expr =
     identifier * simple_binder list * constr_ast * constr_ast
 type cofixpoint_expr =
     identifier * constr_ast * constr_ast
+type local_binder =
+  | LocalRawDef of identifier * constr_ast
+  | LocalRawAssum of identifier list * constr_ast
+type definition_expr =
+  | ProveBody of local_binder list * constr_ast
+  | DefineBody of local_binder list * raw_red_expr option * constr_ast
+      * constr_ast option
 
 type local_decl_expr =
   | AssumExpr of identifier * constr_ast
@@ -174,11 +181,10 @@ type vernac_expr =
   | VernacDistfix of grammar_associativity * int * string * qualid located
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * identifier *
-      raw_red_expr option * constr_ast * constr_ast option *
+  | VernacDefinition of definition_kind * identifier * definition_expr *
+      Proof_type.declaration_hook
+  | VernacStartTheoremProof of theorem_kind * identifier * Coqast.t * bool *
       Proof_type.declaration_hook
-  | VernacStartProof of goal_kind * identifier option *
-      constr_ast * bool * Proof_type.declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
   | VernacExactProof of constr_ast
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
@@ -245,7 +251,7 @@ type vernac_expr =
   | VernacNop
 
   (* Proof management *)
-(*  | VernacGoal of constr_ast option*)
+  | VernacGoal of constr_ast
   | VernacAbort of identifier option
   | VernacAbortAll
   | VernacRestart