Added support for definition of fixpoints using tactics.

Fixed some bugs in -beautify and robustness of {struct} clause.

Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.



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

6 files changed, 197 insertions, 121 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d59b16d823..50cc702e21 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -446,7 +446,7 @@ let check_mutuality env isfix fixl =
 type structured_fixpoint_expr = {
   fix_name : identifier;
   fix_binders : local_binder list;
-  fix_body : constr_expr;
+  fix_body : constr_expr option;
   fix_type : constr_expr
 }
 
@@ -457,9 +457,10 @@ let interp_fix_ccl evdref (env,_) fix =
   interp_type_evars evdref env fix.fix_type
 
 let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
-  let env = push_rel_context ctx env_rec in
-  let body = interp_casted_constr_evars evdref env ~impls fix.fix_body ccl in
-  it_mkLambda_or_LetIn body ctx
+  Option.map (fun body ->
+    let env = push_rel_context ctx env_rec in
+    let body = interp_casted_constr_evars evdref env ~impls body ccl in
+    it_mkLambda_or_LetIn body ctx) fix.fix_body
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
@@ -483,29 +484,19 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let rel_index n ctx =
-  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
-
-let rec unfold f b =
-  match f b with
-    | Some (x, b') -> x :: unfold f b'
-    | None -> []
-
-let compute_possible_guardness_evidences n fixctx fixtype =
-  match n with
-  | Some (loc, n) -> [rel_index n fixctx]
+let compute_possible_guardness_evidences n fix =
+  match index_of_annot fix.fix_binders n with
+  | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      let len = List.length fixctx in
-	unfold (function x when x = len -> None
-	  | n -> Some (n, succ n)) 0
+      interval 0 (local_assums_length fix.fix_binders - 1)
 
 type recursive_preentry =
-  identifier list * constr list * types list
+  identifier list * constr option list * types list
 
 let interp_recursive isfix fixl notations =
   let env = Global.env() in
@@ -532,53 +523,79 @@ let interp_recursive isfix fixl notations =
 
   (* Instantiate evars and check all are resolved *)
   let evd,_ = consider_remaining_unif_problems env_rec !evdref in
-  let fixdefs = List.map (nf_evar evd) fixdefs in
+  let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
+  let fixctxlength = List.map (fun (_,ctx) -> rel_context_nhyps ctx) fixctxs in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
-  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+  List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
-  check_mutuality env isfix (List.combine fixnames fixdefs);
+  if not (List.mem None fixdefs) then begin
+    let fixdefs = List.map Option.get fixdefs in
+    check_mutuality env isfix (List.combine fixnames fixdefs)
+  end;
 
   (* Build the fix declaration block *)
-  let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
-  (snd (List.split fixctxs),fixnames,fixdecls,fixtypes),fiximps
-
-let interp_fixpoint fixl wfl notations =
-  let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
-    interp_recursive true fixl notations in
-  let indexes, fixdecls =
-    let possible_indexes =
-      list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
-	let indexes =
-	  search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
-	Some indexes,
-	list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames
-  in
-  ((fixnames,fixdecls,fixtypes),fiximps,indexes)
-
-let interp_cofixpoint fixl notations =
-  let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
-    interp_recursive false fixl notations in
-  let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-  ((fixnames,fixdecls,fixtypes),fiximps)
-
-let declare_fixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps,indexes) ntns =
-  ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  fixpoint_message indexes fixnames;
+  (fixnames,fixdefs,fixtypes),List.combine fixctxlength fiximps
+
+let interp_fixpoint = interp_recursive true
+let interp_cofixpoint = interp_recursive false
+
+let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+  if List.mem None fixdefs then
+    (* Some bodies to define by proof *)
+    let thms =
+      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+    let init_tac =
+      Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+        fixdefs) in
+    Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
+      (Some(false,indexes,init_tac)) thms (fun _ _ -> ())
+  else begin
+    (* We shortcut the proof process *)
+    let fixdefs = List.map Option.get fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+    let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
+    let fiximps = List.map snd fiximps in
+    let fixdecls =
+      list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+    ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
+    (* Declare the recursive definitions *)
+    fixpoint_message (Some indexes) fixnames;
+  end;
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps) ntns =
-  ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  cofixpoint_message fixnames;
+let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+  if List.mem None fixdefs then
+    (* Some bodies to define by proof *)
+    let thms =
+      list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+    let init_tac =
+      Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+        fixdefs) in
+    Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
+      (Some(true,[],init_tac)) thms (fun _ _ -> ())
+  else begin
+    (* We shortcut the proof process *)
+    let fixdefs = List.map Option.get fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+    let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+    let fiximps = List.map snd fiximps in
+    ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
+    (* Declare the recursive definitions *)
+    cofixpoint_message fixnames
+  end;
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
+let extract_decreasing_argument = function
+  | (_,(na,CStructRec),_,_,_) -> na
+  | _ -> error 
+      "Only structural decreasing is supported for a non-Program Fixpoint"
+
 let extract_fixpoint_components l =
   let fixl, ntnl = List.split l in
-  let wfl = List.map (fun (_,wf,_,_,_) -> fst wf) fixl in
+  let wfl = List.map extract_decreasing_argument fixl in
   let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
     {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
   fixl, List.flatten ntnl, wfl
@@ -591,7 +608,9 @@ let extract_cofixpoint_components l =
 
 let do_fixpoint l b =
   let fixl,ntns,wfl = extract_fixpoint_components l in
-  declare_fixpoint b (interp_fixpoint fixl wfl ntns) ntns
+  let possible_indexes =
+      List.map2 compute_possible_guardness_evidences wfl fixl in
+  declare_fixpoint b (interp_fixpoint fixl ntns) possible_indexes ntns
 
 let do_cofixpoint l b =
   let fixl,ntns = extract_cofixpoint_components l in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index e42580c2b4..48fc5a8ebc 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -20,6 +20,7 @@ open Topconstr
 open Decl_kinds
 open Redexpr
 open Constrintern
+open Pfedit
 (*i*)
 
 (*s This file is about the interpretation of raw commands into typed
@@ -102,7 +103,7 @@ val do_mutual_inductive :
 type structured_fixpoint_expr = {
   fix_name : identifier;
   fix_binders : local_binder list;
-  fix_body : constr_expr;
+  fix_body : constr_expr option;
   fix_type : constr_expr
 }
 
@@ -118,27 +119,27 @@ val extract_cofixpoint_components :
   (cofixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list
 
-(* Typing fixpoints and cofixpoint_expr *)
+(* Typing global fixpoints and cofixpoint_expr *)
 
 type recursive_preentry =
-  identifier list * constr list * types list
+  identifier list * constr option list * types list
 
 val interp_fixpoint :
-  structured_fixpoint_expr list -> lident option list -> decl_notation list ->
-    recursive_preentry * manual_implicits list * int array option
+  structured_fixpoint_expr list -> decl_notation list ->
+    recursive_preentry * (int * manual_implicits) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * manual_implicits list
+    recursive_preentry * (int * manual_implicits) list
 
 (* Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  bool -> recursive_preentry * manual_implicits list * int array option ->
-    decl_notation list -> unit
+  bool -> recursive_preentry * (int * manual_implicits) list -> 
+  lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  bool -> recursive_preentry * manual_implicits list ->
+  bool -> recursive_preentry * (int * manual_implicits) list ->
     decl_notation list -> unit
 
 (* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index d9a26b427f..48666c5145 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -33,6 +33,7 @@ open Reductionops
 open Topconstr
 open Constrintern
 open Impargs
+open Tacticals
 
 (* Support for mutually proved theorems *)
 
@@ -44,26 +45,43 @@ let retrieve_first_recthm = function
       (Option.map Declarations.force body,opaq)
   | _ -> assert false
 
-let adjust_guardness_conditions const =
+let adjust_guardness_conditions const = function
+  | [] -> const (* Not a recursive statement *)
+  | possible_indexes ->
   (* Try all combinations... not optimal *)
   match kind_of_term const.const_entry_body with
   | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-      let possible_indexes =
-	List.map (fun c ->
+(*      let possible_indexes =
+	List.map2 (fun i c -> match i with Some i -> i | None ->
 	  interval 0 (List.length ((lam_assum c))))
-	  (Array.to_list fixdefs) in
+	  lemma_guard (Array.to_list fixdefs) in
+*)
       let indexes =
 	search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
       { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
   | c -> const
 
-let look_for_mutual_statements thms =
-  if List.tl thms <> [] then
-    (* More than one statement: we look for a common inductive hyp or a *)
-    (* common coinductive conclusion *)
+let find_mutually_recursive_statements thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,_) as x) ->
+    let inds = List.map (fun (id,(t,impls,annot)) ->
       let (hyps,ccl) = decompose_prod_assum t in
+      let x = (id,(t,impls)) in
+      match annot with
+      (* Explicit fixpoint decreasing argument is given *)
+      | Some (Some (_,id),CStructRec) ->
+          let i,b,typ = lookup_rel_id id hyps in
+          (match kind_of_term t with
+          | Ind (kn,_ as ind) when
+              let mind = Global.lookup_mind kn in
+              mind.mind_finite & b = None ->
+              [ind,x,i],[]
+          | _ ->
+              error "Decreasing argument is not an inductive assumption.")
+      (* Unsupported cases *)
+      | Some (_,(CWfRec _|CMeasureRec _)) ->
+          error "Only structural decreasing is supported for mutual statements."
+      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
+      | None | Some (None, CStructRec) ->
       let whnf_hyp_hds = map_rel_context_in_env
         (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
         (Global.env()) hyps in
@@ -75,7 +93,7 @@ let look_for_mutual_statements thms =
                 mind.mind_finite & b = None ->
               [ind,x,i]
           | _ ->
-              []) 1 (List.rev whnf_hyp_hds)) in
+              []) 0 (List.rev whnf_hyp_hds)) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
         let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
@@ -102,7 +120,7 @@ let look_for_mutual_statements thms =
       list_cartesians_filter (fun hyp oks ->
 	if List.for_all (of_same_mutind hyp) oks
 	then Some (hyp::oks) else None) [] inds_hyps in
-    let ordered_inds,finite =
+    let ordered_inds,finite,guard =
       match ordered_same_indccl, common_same_indhyp with
       | indccl::rest, _ ->
 	  assert (rest=[]);
@@ -110,37 +128,36 @@ let look_for_mutual_statements thms =
 	  if common_same_indhyp <> [] then
 	    if_verbose warning "Assuming mutual coinductive statements.";
 	  flush_all ();
-          indccl, true
+          indccl, true, []
       | [], _::_ ->
 	  if same_indccl <> [] &&
 	     list_distinct (List.map pi1 (List.hd same_indccl)) then
 	    if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+          let possible_guards = List.map (List.map pi3) inds_hyps in
 	  (* assume the largest indices as possible *)
-	  list_last common_same_indhyp, false
+	  list_last common_same_indhyp, false, possible_guards
       | _, [] ->
 	  error
             ("Cannot find common (mutual) inductive premises or coinductive" ^
              " conclusions in the statements.")
     in
-    let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
-    let rec_tac =
-      if finite then
-        match List.map (fun (id,(t,_)) -> (id,t)) thms with
-        | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
-        | _ -> assert false
-      else
-	(* nl is dummy: it will be recomputed at Qed-time *)
-        match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
-        | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
-        | _ -> assert false in
-    Some rec_tac,thms
-  else
-    None, thms
+    (finite,guard,None), List.map pi2 ordered_inds
+
+let look_for_possibly_mutual_statements = function
+  | [id,(t,impls,None)] ->
+      (* One non recursively proved theorem *)
+      None,[id,(t,impls)]
+  | _::_ as thms ->
+    (* More than one statement and/or an explicit decreasing mark: *)
+    (* we look for a common inductive hyp or a common coinductive conclusion *)
+    let recguard,thms = find_mutually_recursive_statements thms in
+    Some recguard,thms
+  | [] -> anomaly "Empty list of theorems."
 
 (* Saving a goal *)
 
 let save id const do_guard (locality,kind) hook =
-  let const = if do_guard then adjust_guardness_conditions const else const in
+  let const = adjust_guardness_conditions const do_guard in
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
@@ -221,9 +238,6 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
     error "This command can only be used for unnamed theorem."
-(*
-    message("Overriding name "^(string_of_id id)^" and using "^save_ident)
-*)
 
 let save_anonymous opacity save_ident =
   let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
@@ -243,26 +257,47 @@ let save_anonymous_with_strength kind opacity save_ident =
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
-let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
+let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
   !start_hook c;
   Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
 
-let start_proof_com kind thms hook =
-  let evdref = ref (create_evar_defs Evd.empty) in
-  let env = Global.env () in
-  let thms = List.map (fun (sopt,(bl,t)) ->
-    let (env, ctx), imps = interp_context_evars evdref env bl in
-    let t', imps' = interp_type_evars_impls ~evdref env t in
-    let len = List.length ctx in
-      (compute_proof_name sopt,
-      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'))))
-    thms in
-  let rec_tac,thms = look_for_mutual_statements thms in
+let rec_tac_initializer finite guard thms =
+  if finite then
+    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+    | _ -> assert false
+  else
+    (* nl is dummy: it will be recomputed at Qed-time *)
+    let nl = List.map succ (List.map list_last guard) in
+    match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+    | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+    | _ -> assert false
+
+let start_proof_with_initialization kind recguard thms hook =
+  let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
+  let init_tac,guard = match recguard with
+  | Some (finite,guard,init_tac) ->
+      let rec_tac = rec_tac_initializer finite guard thms in
+      Some (match init_tac with
+        | None -> 
+            if Flags.is_auto_intros () then 
+              tclTHENS rec_tac (List.map intro_tac thms)
+            else
+              rec_tac
+        | Some tacl ->
+            tclTHENS rec_tac
+            (if Flags.is_auto_intros () then
+              List.map2 (fun tac thm -> tclTHEN tac (intro_tac thm)) tacl thms
+            else
+              tacl)),guard
+  | None ->
+      assert (List.length thms = 1);
+      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly "No proof to start"
-  | (id,(t,(len,imps)) as thm)::other_thms ->
+  | (id,(t,(len,imps)))::other_thms ->
       let hook strength ref =
         let other_thms_data =
           if other_thms = [] then [] else
@@ -273,14 +308,22 @@ let start_proof_com kind thms hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      let init_tac =
-       let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
-         if Flags.is_auto_intros () then
-           match rec_tac with
-           | None -> Some (intro_tac thm)
-           | Some tac -> Some (Tacticals.tclTHENS tac (List.map intro_tac thms))
-         else rec_tac
-      in start_proof id kind t ?init_tac hook ~compute_guard:(rec_tac<>None)
+      start_proof id kind t ?init_tac hook ~compute_guard:guard
+
+let start_proof_com kind thms hook =
+  let evdref = ref (create_evar_defs Evd.empty) in
+  let env = Global.env () in
+  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+    let (env, ctx), imps = interp_context_evars evdref env bl in
+    let t', imps' = interp_type_evars_impls ~evdref env t in
+    let len = List.length ctx in
+      (compute_proof_name sopt,
+      (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
+       (len, imps @ lift_implicits len imps'),
+       guard)))
+    thms in
+  let recguard,thms = look_for_possibly_mutual_statements thms in
+  start_proof_with_initialization kind recguard thms hook
 
 (* Admitted *)
 
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 398b336be0..5d4f014a36 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -3,7 +3,7 @@
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*         *       GNU Lesser General Public License Version 2.fix_expr        *)
 (************************************************************************)
 
 (*i $Id$ i*)
@@ -16,16 +16,23 @@ open Topconstr
 open Tacexpr
 open Vernacexpr
 open Proof_type
+open Pfedit
 (*i*)
 
 (* A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : identifier -> goal_kind -> types ->
-  ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+  ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
+    declaration_hook -> unit
 
 val start_proof_com : goal_kind ->
-  (lident option * (local_binder list * constr_expr)) list ->
+  (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+  declaration_hook -> unit
+
+val start_proof_with_initialization : 
+  goal_kind -> (bool * lemma_possible_guards * tactic list option) option ->
+  (identifier * (types * (int * Impargs.manual_explicitation list))) list ->
   declaration_hook -> unit
 
 (* A hook the next three functions pass to cook_proof *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a37e3e5df1..e7d32782d6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -313,7 +313,7 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook =
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	let hook _ _ = () in
  	  start_proof_and_print (local,DefinitionBody Definition)
-	    [Some lid, (bl,t)] hook
+	    [Some lid, (bl,t,None)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
@@ -1402,7 +1402,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->())
+  | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] 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 6148b98aee..f75e1771d8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -150,6 +150,12 @@ type definition_expr =
   | DefineBody of local_binder list * raw_red_expr option * constr_expr
       * constr_expr option
 
+type fixpoint_expr =
+    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+
+type cofixpoint_expr =
+    identifier located * local_binder list * constr_expr * constr_expr option
+
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
@@ -218,7 +224,7 @@ type vernac_expr =
   | VernacDefinition of definition_kind * lident * definition_expr *
       declaration_hook
   | VernacStartTheoremProof of theorem_kind *
-      (lident option * (local_binder list * constr_expr)) list *
+      (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
         bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr