From 17550e80aa0c7fbeaec13d46629c92de6967b1d1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 2 Sep 2008 21:36:06 +0000
Subject: 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
---
 theories/Program/Equality.v | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 44d2f4f7e4..869df369b8 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".
 
-- 
cgit v1.2.3