From 73e85bb97b86c53f34b984d0193835c1d722c59f Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 3 Sep 2008 14:47:14 +0000
Subject: Better handling of recursive Equations definitions... still not
 perfect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11356 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/equations.ml4 |  1 +
 theories/Program/Equality.v  | 21 +++++++++++++++------
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 4464d1ca63..14330e72eb 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -666,6 +666,7 @@ let define_by_eqs i l t nt eqs =
   let prob = (i, sign, arity) in
   let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
   let ce = check_evars fixenv Evd.empty !isevar in
+  List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations;
   let is_recursive, env' =
     let occur_eqn (ctx, _, rhs) =
       match rhs with
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 2bf25c8e70..d11996a672 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -408,10 +407,10 @@ Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse.
 (** Solving a method call: we must refine the goal until the body 
    can be applied or just solve it by splitting on an empty family member. *)
     
-Ltac solve_method :=
+Ltac solve_method rec :=
   match goal with
     | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body
-    | [ H := ?body |- _ ] => simplify_method H ; (try intro) ; try_intros body
+    | [ H := ?body |- _ ] => simplify_method H ; rec ; try_intros body
   end.
 
 (** Impossible cases, by splitting on a given target. *)
@@ -429,9 +428,19 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
+Ltac nonrec_equations := 
+  solve [solve_equations (solve_method idtac)] || solve [ solve_split ]
+    || fail "Unnexpected equations goal".
+
+Ltac recursive_equations :=
+  solve [solve_equations (solve_method ltac:intro)] || solve [ solve_split ] 
+    || fail "Unnexpected recursive equations goal".
+
 (** The [equations] tactic is the toplevel tactic for solving goals generated
    by [Equations]. *)
 
-Ltac equations := intro_prototypes ;
-  solve [solve_equations solve_method] || solve [ solve_split ] || fail "Unnexpcted equations goal".
-
+Ltac equations :=
+  match goal with 
+    | [ |- Π x : _, _ ] => intro ; recursive_equations
+    | _ => nonrec_equations
+  end.
-- 
cgit v1.2.3