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

5 files changed, 22 insertions, 9 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bd3f7e8ec8..781a841c95 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 9ba1d6715c..5f3b6b28d4 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 2db2533737..b337d33520 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 c63e8488bb..dc57e4aadc 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 3e275cd0fd..7d1f2cd62e 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