Cleanup in subtac_cases, preparing to use improvements on return predicate

inference. Little improvement un subtac_obligations: do not retry to
solve all obligations when finishing to solve one obligation nobody
depends on.


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

1 files changed, 4 insertions, 4 deletions

diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 97cef9a503..da612c4367 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -1,6 +1,6 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 
 Set Implicit Arguments.
 
@@ -23,13 +23,13 @@ Section Map_DependentRecursor.
   Variable f : { x : U | In x l } -> V.
 
   Obligations Tactic := unfold sub_list in * ; 
-    subtac_simpl ; intuition.
+    program_simpl ; intuition.
 
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
     { measure length l' } : { r : list V | length r = length l' } :=
     match l' with
-    nil => nil
-    | cons x tl => let tl' := map_rec tl in
+      | nil => nil
+      | cons x tl => let tl' := map_rec tl in
 	f x :: tl'
     end.