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

28 files changed, 374 insertions, 252 deletions

diff --git a/CHANGES b/CHANGES
index b6744e25d..627408cc8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,6 +42,9 @@ Tactics
 - A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle.
   This tactic is simply a shortcut for "elimtype False".
 - Added support for Leibniz-rewriting of dependent hypotheses.
+- Binders given before ":" in lemmas are now automatically
+  introduced in the context (possible source of incompatibility that can be
+  avoided by unsetting option "Automatic Introduction").
 
 Tactic Language
 
@@ -75,6 +78,7 @@ Vernacular commands
 - Made support for automatic generation of case analysis schemes and
   congruence schemes available to user (governed by options "Unset
   Case Analysis Schemes" and "Unset Congruence Schemes").
+- Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
 
 Tools
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 85f84b850..e819e7009 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1048,11 +1048,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg f =
-	       let idx =
-		 match n with
-		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
-		   | None -> 0
-	       in
+               let idx = Option.default 0 (index_of_annot bl n) in
 	       let before, after = list_chop idx bl in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a6b4b1b0a..ecb61e15b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -639,8 +639,8 @@ type cases_pattern_expr =
 
 type constr_expr =
   | CRef of reference
-  | CFix of loc * identifier located * fixpoint_expr list
-  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CFix of loc * identifier located * fix_expr list
+  | CCoFix of loc * identifier located * cofix_expr list
   | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -667,7 +667,7 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr =
+and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
@@ -678,7 +678,7 @@ and typeclass_constraint = name located * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
-and cofixpoint_expr =
+and cofix_expr =
     identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr =
@@ -918,6 +918,19 @@ let coerce_to_name = function
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
 
+(* Interpret the index of a recursion order annotation *)
+
+let index_of_annot bl na =
+  let names = List.map snd (names_of_local_assums bl) in
+  match na with
+  | None ->
+      if names = [] then error "A fixpoint needs at least one parameter." 
+      else None
+  | Some (loc, id) ->
+      try Some (list_index0 (Name id) names)
+      with Not_found ->
+        user_err_loc(loc,"",
+        str "No parameter named " ++ Nameops.pr_id id ++ str".")
 
 (* Used in correctness and interface *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1c0b207ea..b7e389d6b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,8 +125,8 @@ type cases_pattern_expr =
 
 type constr_expr =
   | CRef of reference
-  | CFix of loc * identifier located * fixpoint_expr list
-  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CFix of loc * identifier located * fix_expr list
+  | CCoFix of loc * identifier located * cofix_expr list
   | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -153,10 +153,10 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr =
+and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
-and cofixpoint_expr =
+and cofix_expr =
     identifier located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr =
@@ -205,6 +205,8 @@ val coerce_reference_to_id : reference -> identifier
 val coerce_to_id : constr_expr -> identifier located
 val coerce_to_name : constr_expr -> name located
 
+val index_of_annot : local_binder list -> identifier located option -> int option
+
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
@@ -220,12 +222,12 @@ val local_binders_length : local_binder list -> int
 (* Excludes let binders *)
 val local_assums_length : local_binder list -> int
 
-(* Does not take let binders into account *)
-val names_of_local_assums : local_binder list -> name located list
-
 (* With let binders *)
 val names_of_local_binders : local_binder list -> name located list
 
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
 (* Used in typeclasses *)
 
 val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
diff --git a/lib/flags.ml b/lib/flags.ml
index 971b560ec..555739b11 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -65,7 +65,7 @@ let if_verbose f x = if not !silent then f x
 
 let auto_intros = ref false
 let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = !auto_intros
+let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
 let hash_cons_proofs = ref true
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 669d1f2ae..393125e29 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -10,6 +10,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Pcoq
 open Constr
 open Prim
@@ -43,21 +44,11 @@ let binders_of_lidents l =
     LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
 		  CHole (loc, Some (Evd.BinderType (Name id))))) l
 
-let rec index_and_rec_order_of_annot loc bl ann =
-  match names_of_local_assums bl,ann with
-    | [loc,Name id], (None, r) -> Some (loc, id), r
-    | lids, (Some (loc, n), ro) ->
-        if List.exists (fun (_, x) -> x = Name n) lids then
-	  Some (loc, n), ro
-        else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.")
-    | _, (None, r) -> None, r
-
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
-  let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None) in
-  (id,(n,ro),bl,ty,body)
+  (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
@@ -308,7 +299,8 @@ GEXTEND Gram
   ;
   fix_decl:
     [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
-        c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
+        c=operconstr LEVEL "200" ->
+          (id,fst bl,snd bl,c,ty) ] ]
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
@@ -402,8 +394,7 @@ GEXTEND Gram
     [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
 	(assum (loc, Name id) :: fst bl), snd bl
     | f = fixannot -> [], f
-    | b = binder_let; bl = binders_let_fixannot ->
-	b @ fst bl, snd bl
+    | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
     | -> [], (None, CStructRec)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56946ef27..54cf671cc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -129,8 +129,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
-            (Some id,(bl,c)) ] ->
-          VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
+            (Some id,(bl,c,None)) ] ->
+          VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | stre = assumptions_token; nl = inline; bl = assum_list ->
@@ -275,29 +275,12 @@ GEXTEND Gram
     [ [ id = identref;
 	bl = binders_let_fixannot;
         ty = type_cstr;
-	":="; def = lconstr; ntn = decl_notation ->
-	  let bl, annot = bl in
-          let names = names_of_local_assums bl in
-          let ni =
-            match fst annot with
-                Some (loc, id) ->
-                  (if List.exists (fun (_, id') -> Name id = id') names then
-		    Some (loc, id)
-		    else Util.user_err_loc
-                      (loc,"Fixpoint",
-                       str "No argument named " ++ Nameops.pr_id id ++ str"."))
-              | None ->
-		  (* If there is only one argument, it is the recursive one,
-		     otherwise, we search the recursive index later *)
-		  match names with
-		    | [(loc, Name na)] -> Some (loc, na)
-		    | _ -> None
-	  in
-	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
+	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
+	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = identref; bl = binders_let; ty = type_cstr; ":=";
-        def = lconstr; ntn = decl_notation ->
+    [ [ id = identref; bl = binders_let; ty = type_cstr; 
+        def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
   type_cstr:
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 190271159..4f31607aa 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -302,6 +302,28 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
+let names_of_binder = function
+  | LocalRawAssum (nal,_,_) -> nal
+  | LocalRawDef (_,_) -> []
+
+let pr_guard_annot bl (n,ro) =
+  match n with
+  | None -> mt ()
+  | Some (loc, id) ->
+      match (ro : Topconstr.recursion_order_expr) with
+      | CStructRec ->
+          let ids = List.flatten (List.map names_of_binder bl) in
+	  if List.length ids > 1 then
+	    spc() ++ str "{struct " ++ pr_id id ++ str"}"
+	  else mt()
+      | CWfRec c ->
+	  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
+	  pr_id id ++ str"}"
+      | CMeasureRec (m,r) ->
+	  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
+	  pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
+	    pr_lconstr_expr r) ++ str"}"
+
 let pr_onescheme (idop,schem) =
   match schem with
   | InductionScheme (dep,ind,s) ->
@@ -409,6 +431,14 @@ let pr_paren_reln_or_extern = function
   | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
 
+let pr_statement head (id,(bl,c,guard)) =
+  assert (id<>None);
+  hov 0
+    (head ++ pr_lident (Option.get id) ++ spc() ++
+    (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+    pr_opt (pr_guard_annot bl) guard ++
+    str":" ++ pr_spc_lconstr c)
+
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
@@ -567,11 +597,6 @@ let rec pr_vernac = function
         | Some cc -> str" :=" ++ spc() ++ cc))
 
   | VernacStartTheoremProof (ki,l,_,_) ->
-      let pr_statement head (id,(bl,c)) =
-        hov 0
-          (head ++ pr_opt pr_lident id ++ spc() ++
-              (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-              str":" ++ pr_spc_lconstr c) in
       hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
              prlist (pr_statement (spc () ++ str "with")) (List.tl l))
 
@@ -605,75 +630,46 @@ let rec pr_vernac = function
 	    spc() ++
 	    pr_record_decl b c fs in
       let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
-	let kw =
-	  str (match k with Record -> "Record" | Structure -> "Structure"
-		 | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-		 | Class b -> if b then "Definitional Class" else "Class")
-	in
-	  hov 0 (
-	    kw ++ spc() ++
-	      (if i then str"Infer" else str"") ++
-              (if coe then str" > " else str" ") ++ pr_lident id ++
+	hov 0 (
+	    str key ++ spc() ++
+	      (if i then str"Infer " else str"") ++
+              (if coe then str"> " else str"") ++ pr_lident id ++
               pr_and_type_binders_arg indpar ++ spc() ++
 	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
 	      str" :=") ++ pr_constructor_list k lc ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
-      hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
-      ++
+      let key =
+        let (_,_,_,k,_),_ = List.hd l in
+	match k with Record -> "Record" | Structure -> "Structure"
+	  | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+	  | Class b -> if b then "Definitional Class" else "Class" in
+      hov 1 (pr_oneind key (List.hd l)) ++
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
 
   | VernacFixpoint (recs,b) ->
-      let name_of_binder = function
-        | LocalRawAssum (nal,_,_) -> nal
-        | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | ((loc,id),(n,ro),bl,type_,def),ntn ->
-            let (bl',def,type_) =
-              if Flags.do_beautify() then extract_def_binders def type_
-              else ([],def,type_) in
-            let bl = bl @ bl' in
-            let ids = List.flatten (List.map name_of_binder bl) in
-            let annot =
-	      match n with
-		| None -> mt ()
-		| Some (loc, id) ->
-		    match (ro : Topconstr.recursion_order_expr) with
-			CStructRec ->
-			  if List.length ids > 1 then
-			    spc() ++ str "{struct " ++ pr_id id ++ str"}"
-			  else mt()
-		      | CWfRec c ->
-			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
-			    pr_id id ++ str"}"
-		      | CMeasureRec (m,r) ->
-			  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
-			    pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
-			    pr_lconstr_expr r) ++ str"}"
-	    in
+        | ((loc,id),ro,bl,type_,def),ntn ->
+            let annot = pr_guard_annot bl ro in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++
+            ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
       let start = if b then "Boxed Fixpoint" else "Fixpoint" in
-      hov 1 (str start ++ spc() ++
-        prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
+      hov 0 (str start ++ spc() ++
+        prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
-        let (bl',def,c) =
-              if Flags.do_beautify() then extract_def_binders def c
-              else ([],def,c) in
-        let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
-        str" :=" ++ brk(1,1) ++ pr_lconstr def  ++
+        pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	prlist (pr_decl_notation pr_constr) ntn
       in
       let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
-      hov 1 (str start ++ spc() ++
+      hov 0 (str start ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bd3f7e8ec..781a841c9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -372,6 +372,9 @@ let register_struct is_rec fixpoint_exprl =
 	  fname (Decl_kinds.Global,Decl_kinds.Definition)
 	  ce imps (fun _ _ -> ())
     | _ ->
+        let fixpoint_exprl =
+          List.map (fun ((name,annot,bl,types,body),ntn) ->
+            ((name,annot,bl,types,Some body),ntn)) fixpoint_exprl in
 	Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 9ba1d6715..5f3b6b28d 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1917,7 +1917,7 @@ let rec xlate_vernac =
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
+  | VernacStartTheoremProof (k, [Some (_,s), (bl,c,None)], _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
@@ -1993,9 +1993,10 @@ let rec xlate_vernac =
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
       let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
+        if ardef = None then xlate_error "Fixpoint proved by tactics";
         let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
-        let ardef = xlate_formula ardef in
+        let ardef = xlate_formula (Option.get ardef) in
 	match xlate_binder_list bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
@@ -2006,8 +2007,9 @@ let rec xlate_vernac =
    | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
    | VernacCoFixpoint ((lm :: lmi),boxed) ->
       let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
+        if ardef = None then xlate_error "Fixpoint proved by tactics";
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
-                      xlate_formula arf, xlate_formula ardef) in
+                      xlate_formula arf, xlate_formula (Option.get ardef)) in
         CT_cofix_decl
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
    | VernacScheme [] -> xlate_error "induction scheme"
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 2db253373..b337d3352 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -152,7 +152,9 @@ let subtac (loc, command) =
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l b)
 
-  | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
+  | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
+      if guard <> None then 
+        error "Do not support building theorems as a fixpoint.";
       Dumpglob.dump_definition id false "prf";
       if not(Pfedit.refining ()) then
 	if lettop then
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index c63e8488b..dc57e4aad 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -365,8 +365,8 @@ let interp_fix_ccl evdref (env,_) fix =
 
 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.Command.fix_body ccl in
-  it_mkLambda_or_LetIn body ctx
+  let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
+  Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
@@ -416,6 +416,10 @@ let check_evars env initial_sigma evd c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
+let out_def = function
+  | Some def -> def
+  | None -> error "Program Fixpoint needs defined bodies."
+
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
@@ -452,6 +456,8 @@ let interp_recursive fixkind l boxed =
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
 
+  let fixdefs = List.map out_def fixdefs in
+
   (* Instantiate evars and check all are resolved *)
   let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
   let evd = Typeclasses.resolve_typeclasses
@@ -507,14 +513,14 @@ let build_recursive l b =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
 	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, n, bl, typ, def) r
+	  ignore(build_wellfounded (id, n, bl, typ, out_def def) r
 		    (match n with Some n -> mkIdentC (snd n) | None ->
 		      errorlabstrm "Subtac_command.build_recursive"
 			(str "Recursive argument required for well-founded fixpoints"))
 		    ntn false)
 
       | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, n, bl, typ, def) (Option.default (CRef lt_ref) r)
+	  ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
 		    m ntn false)
 
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 3e275cd0f..7d1f2cd62 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -110,7 +110,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let pretype_id loc env (lvar,unbndltacvars) id =
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
-	let (n,typ) = lookup_rel_id id (rel_context env) in
+	let (n,_,typ) = lookup_rel_id id (rel_context env) in
 	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ae7106fb3..177389c98 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1316,7 +1316,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
     (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
-    let (p,_) = lookup_rel_id x (rel_context extenv) in
+    let (p,_,_) = lookup_rel_id x (rel_context extenv) in
     let rec aux n (_,b,ty) =
       match b with
       | Some c ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 10d9a1c4e..288eb9da2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -230,7 +230,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let pretype_id loc env (lvar,unbndltacvars) id =
     try
-      let (n,typ) = lookup_rel_id id (rel_context env) in
+      let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
     with Not_found ->
     try
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 81c740580..4de4bde2c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -221,7 +221,7 @@ let push_named_rec_types (lna,typarray,_) env =
 let rec lookup_rel_id id sign =
   let rec lookrec = function
     | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
-    | (n, (Name id',_,t)::l)  -> if id' = id then (n,t) else lookrec (n+1,l)
+    | (n, (Name id',b,t)::l)  -> if id' = id then (n,b,t) else lookrec (n+1,l)
     | (_, [])                 -> raise Not_found
   in
   lookrec (1,sign)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 7f9ccb28e..59f7750d3 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -39,7 +39,7 @@ val print_env : env -> std_ppcmds
 val push_rel_assum : name * types -> env -> env
 val push_rels_assum : (name * types) list -> env -> env
 val push_named_rec_types : name array * types array * 'a -> env -> env
-val lookup_rel_id : identifier -> rel_context -> int * types
+val lookup_rel_id : identifier -> rel_context -> int * constr option * types
 
 (* builds argument lists matching a block of binders or a context *)
 val rel_vect : int -> int -> constr array
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7895bfac9..f3658ad4b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -31,10 +31,12 @@ open Safe_typing
 (* Mainly contributed by C. Murthy                                   *)
 (*********************************************************************)
 
+type lemma_possible_guards = int list list
+
 type proof_topstate = {
   mutable top_end_tac : tactic option;
   top_init_tac : tactic option;
-  top_compute_guard : bool;
+  top_compute_guard : lemma_possible_guards;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
@@ -252,7 +254,7 @@ let set_end_tac tac =
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook =
   let top_goal = mk_goal sign concl None in
   let ts = {
     top_end_tac = None;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6acf1ff78..acb852471 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -78,9 +78,12 @@ val get_undo : unit -> int option
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
+type lemma_possible_guards = int list list
+
 val start_proof :
   identifier -> goal_kind -> named_context_val -> constr ->
-    ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+  ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
+  declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -108,7 +111,9 @@ val suspend_proof : unit -> unit
     it also tells if the guardness condition has to be inferred. *)
 
 val cook_proof : (Refiner.pftreestate -> unit) ->
-  identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
+  identifier *
+  (Entries.definition_entry * lemma_possible_guards * goal_kind * 
+   declaration_hook)
 
 (* To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 4130a16ca..fcf8d8d4a 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -48,3 +48,44 @@ Fixpoint foldrn n bs :=
 
 End folding.
 
+(* Check definition by tactics *)
+
+Inductive even : nat -> Type :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Type :=
+    odd_S : forall n, even n -> odd (S n).
+
+Fixpoint even_div2 n (H:even n) : nat :=
+  match H with
+  | even_O => 0
+  | even_S n H => S (odd_div2 n H)
+  end
+with odd_div2 n H : nat.
+destruct H.
+apply even_div2 with n.
+assumption.
+Qed.
+
+Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat.
+destruct H.
+exact 0.
+apply odd_div2' with n.
+assumption.
+destruct H.
+apply even_div2' with n.
+assumption.
+Qed.
+
+CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B
+with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B.
+
+CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool
+with ex2 (n:nat) (b:bool) : Stream2 nat bool.
+apply Cons1.
+exact n.
+apply (ex2 n b).
+apply Cons2.
+exact b.
+apply (ex1 (S n) (negb b)).
+Defined.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index deb6f229b..d696360fd 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -22,17 +22,17 @@ Definition zerop n : {n = 0} + {0 < n}.
 Defined.
 
 Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
-  induction n; simple destruct m; auto with arith.
-  intros m0; elim (IHn m0); auto with arith.
-  induction 1; auto with arith.
+  intros; induction n in m |- *; destruct m; auto with arith.
+  destruct (IHn m) as [H|H]; auto with arith.
+  destruct H; auto with arith.
 Defined.
 
 Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
-  exact lt_eq_lt_dec.
+  intros; apply lt_eq_lt_dec; assumption.
 Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
-  induction n.
+  intros; induction n in m |- *.
   auto with arith.
   destruct m.
   auto with arith.
@@ -40,7 +40,7 @@ Definition le_lt_dec n m : {n <= m} + {m < n}.
 Defined.
 
 Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
-  exact le_lt_dec.
+  intros; exact (le_lt_dec n m).
 Defined.
 
 Definition le_ge_dec n m : {n <= m} + {n >= m}.
@@ -48,11 +48,11 @@ Definition le_ge_dec n m : {n <= m} + {n >= m}.
 Defined.
 
 Definition le_gt_dec n m : {n <= m} + {n > m}.
-  exact le_lt_dec.
+  intros; exact (le_lt_dec n m).
 Defined.
 
 Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
-  intros; elim (lt_eq_lt_dec n m); auto with arith.
+  intros; destruct (lt_eq_lt_dec n m); auto with arith.
   intros; absurd (m < n); auto with arith.
 Defined.
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f5d08edb4..f66fa87b6 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -406,7 +406,7 @@ Qed.
 
 Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
   Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
-Proof. unfold Normalizes. intros.
+Proof. unfold Normalizes in *. intros.
   rewrite NA, NB. firstorder.
 Qed.
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d59b16d82..50cc702e2 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 e42580c2b..48fc5a8eb 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 d9a26b427..48666c514 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 398b336be..5d4f014a3 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 a37e3e5df..e7d32782d 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 6148b98ae..f75e1771d 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