Add destruct_call_concl in SubtacTactics and fix obvious obligation handling bug introduced by previous commit

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

2 files changed, 15 insertions, 3 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index 1d4d948ac..0a935c0d2 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -49,6 +49,19 @@ Ltac destruct_call f :=
       end
     end.
 
+Ltac destruct_call_concl f :=
+  match goal with
+    | |- ?T  =>
+      match T with
+        | context [f ?x ?y ?z ?w ?v ?u] => let n := fresh "H" in set (n:=f x y z w v u); destruct n
+        | context [f ?x ?y ?z ?w ?v] => let n := fresh "H" in set (n:=f x y z w v); destruct n
+        | context [f ?x ?y ?z ?w] => let n := fresh "H" in set (n:=f x y z w); destruct n
+        | context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
+        | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
+        | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
+      end
+  end.
+
 Ltac myinjection :=
       let tac H := inversion H ; subst ; clear H in
         match goal with
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d42de1333..b15dd97b1 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -240,9 +240,8 @@ let update_obls prg obls rem =
 		(declare_mutual_definition progs;
 		 from_prg := List.fold_left
 		   (fun acc x -> 
-		      ProgMap.remove x.prg_name acc) !from_prg progs;
-		 true)
-	      else false)
+		      ProgMap.remove x.prg_name acc) !from_prg progs);
+	      false)
 	    
 let is_defined obls x = obls.(x).obl_body <> None