2 files changed, 12 insertions, 7 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,