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

2 files changed, 11 insertions, 4 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7895bfac93..f3658ad4b6 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 6acf1ff780..acb852471d 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