Add support for recursive definitions to [Equations], deciding if a

definition is recursive or not based on occurence of a rec call in 
the body. Examples updated, enjoy!


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

1 files changed, 11 insertions, 3 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 44d2f4f7e..869df369b 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -411,7 +411,7 @@ Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse.
 Ltac solve_method :=
   match goal with
     | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body
-    | [ H := ?body |- _ ] => simplify_method H ; try_intros body
+    | [ H := ?body |- _ ] => simplify_method H ; (try intro) ; try_intros body
   end.
 
 (** Impossible cases, by splitting on a given target. *)
@@ -421,9 +421,17 @@ Ltac solve_split :=
     | [ |- let split := ?x : nat in _ ] => intros _ ; solve_empty x
   end.
 
+(** If defining recursive functions, the prototypes come first. *)
+
+Ltac intro_prototypes :=
+  match goal with 
+    | [ |- Π x : _, _ ] => intro ; intro_prototypes
+    | _ => idtac
+  end.
+
 (** The [equations] tactic is the toplevel tactic for solving goals generated
    by [Equations]. *)
 
-Ltac equations := 
-  solve [ solve_split ] || solve [solve_equations solve_method] || fail "Unnexpcted equations goal".
+Ltac equations := intro_prototypes ;
+  solve [solve_equations solve_method] || solve [ solve_split ] || fail "Unnexpcted equations goal".