Solve obligation handling bug of trying to solve automatically at Next Obligation time. Now done at Qed or Defined.

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

4 files changed, 55 insertions, 90 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index d589c5c1f6..6285599dc8 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -105,8 +105,10 @@ VERNAC COMMAND EXTEND Subtac_Obligations
 END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
-| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
-| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
 | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
 | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
     END
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index a7bb53c593..d42de13334 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -226,19 +226,23 @@ let update_obls prg obls rem =
     from_prg := map_replace prg.prg_name prg' !from_prg;
     if rem > 0 then (
       Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
-    )
+      true)
     else (
       Options.if_verbose msgnl (str "No more obligations remaining");
       match prg'.prg_deps with
 	  [] ->
 	    declare_definition prg';
-	    from_prg := ProgMap.remove prg.prg_name !from_prg
+	    from_prg := ProgMap.remove prg.prg_name !from_prg;
+	    false
 	| l ->
 	    let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
 	      if List.for_all (fun x -> obligations_solved x) progs then 
 		(declare_mutual_definition progs;
 		 from_prg := List.fold_left
-		   (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
+		   (fun acc x -> 
+		      ProgMap.remove x.prg_name acc) !from_prg progs;
+		 true)
+	      else false)
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
@@ -252,8 +256,21 @@ let deps_remaining obls deps =
 let kind_of_opacity o =
   if o then Subtac_utils.goal_proof_kind
   else Subtac_utils.goal_kind
+   
+let obligations_of_evars evars =
+  let arr = 
+    Array.of_list
+      (List.map
+	 (fun (n, t) ->
+	    { obl_name = n;
+	      obl_type = t;
+	      obl_body = None;
+	      obl_opaque = false;
+	      obl_deps = Intset.empty;
+	    }) evars)
+  in arr, Array.length arr
 
-let solve_obligation prg num =
+let rec solve_obligation prg num =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -269,14 +286,15 @@ let solve_obligation prg num =
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
-		     update_obls prg obls (pred rem));
+		     if update_obls prg obls (pred rem) then
+		       auto_solve_obligations (Some prg.prg_name));
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
 	      Pfedit.by !default_tactic
 	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
-let subtac_obligation (user_num, name, typ) =
+and subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
   let prg = get_prog name in
   let obls, rem = prg.prg_obligations in
@@ -287,21 +305,8 @@ let subtac_obligation (user_num, name, typ) =
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
       
-      
-let obligations_of_evars evars =
-  let arr = 
-    Array.of_list
-      (List.map
-	 (fun (n, t) ->
-	    { obl_name = n;
-	      obl_type = t;
-	      obl_body = None;
-	      obl_opaque = false;
-	      obl_deps = Intset.empty;
-	    }) evars)
-  in arr, Array.length arr
-
-let solve_obligation_by_tac prg obls i tac =
+   
+and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
   match obl.obl_body with 
       Some _ -> false
@@ -318,7 +323,7 @@ let solve_obligation_by_tac prg obls i tac =
 	   else false
 	 with _ -> false)  
 
-let solve_obligations n tac = 
+and solve_obligations n tac = 
   let prg = get_prog n in
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
@@ -331,6 +336,12 @@ let solve_obligations n tac =
   in
     update_obls prg obls' !rem
 
+and try_solve_obligations n tac = 
+  ignore (solve_obligations n tac)
+
+and auto_solve_obligations n =
+  try_solve_obligations n !default_tactic
+    
 let add_definition n b t obls =
   Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] (Array.make 0 0) obls in
@@ -343,7 +354,7 @@ let add_definition n b t obls =
     let len = Array.length obls in
     let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      solve_obligations (Some n) !default_tactic)
+      try_solve_obligations (Some n) !default_tactic)
 	
 let add_mutual_definitions l nvrec =
   let deps = List.map (fun (n, b, t, obls) -> n) l in
@@ -354,7 +365,7 @@ let add_mutual_definitions l nvrec =
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps
+    List.iter (fun x -> try_solve_obligations (Some x) !default_tactic) deps
 
 let admit_obligations n =
   let prg = get_prog n in
@@ -369,7 +380,7 @@ let admit_obligations n =
 		   | Some _ -> x)
       obls
   in
-    update_obls prg obls' 0
+    ignore(update_obls prg obls' 0)
 
 exception Found of int
 
@@ -378,17 +389,13 @@ let array_find f arr =
     raise Not_found
   with Found i -> i
 
-let rec next_obligation n =
+let next_obligation n =
   let prg = get_prog n in
   let obls, rem = prg.prg_obligations in
   let i = 
     array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
       obls
-  in
-    if solve_obligation_by_tac prg obls i !default_tactic then (
-      update_obls prg obls (pred rem);
-      next_obligation n
-    ) else solve_obligation prg i
+  in solve_obligation prg i
       
 open Pp
 let show_obligations n =
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 28444e4c9f..16abb47aaf 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -15,7 +15,8 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> bool
+val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit
 
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 948ab8e921..f942292f49 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -21,7 +21,10 @@ Section Map_DependentRecursor.
   Variable U V : Set.
   Variable l : list U.
   Variable f : { x : U | In x l } -> V.
-  Obligations Tactic := idtac.
+
+  Obligations Tactic := unfold sub_list in * ; 
+    subtac_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
@@ -30,62 +33,14 @@ Section Map_DependentRecursor.
 	f x :: tl'
     end.
     
-    Obligation 1.
-    intros.
-    unfold proj1_sig in map_rec.
-    intros.
-    destruct l' ; subtac_simpl.
-    rewrite <- Heq_l'.
-    auto.
-    Qed.
-
-    Obligation 2.
-    simpl.
-    intros.
-    destruct l'.
-    subtac_simpl.
-    inversion s.
-    unfold sub_list. 
-    intuition.
-    Qed.
-
-
-    Obligation 3 of map_rec.
-    simpl.
-    intros.
-    rewrite <- Heq_l'.
+  Next Obligation.
+    destruct_call map_rec.
+    simpl in *.
+    subst x0.
     simpl ; auto with arith.
-    Qed.
-
-    Obligation 4.
-    simpl.
-    intros.
-    destruct l'.
-    simpl in Heq_l'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heq_l'.
-    subst x tl.
-    inversion s.
-    apply H.
-    auto with datatypes.
-    Qed.
-  
-    Obligation 5.
-    Proof.
-      intros.
-      destruct tl'.
-      destruct l'.
-      simpl in *.
-      subst.
-      simpl.
-      subtac_simpl.
-      simpl ; rewrite e ; auto.
-    Qed.
-    
-    Program Definition map : list V := map_rec l.
-    Obligation 1.
-      split ; auto.
-    Qed.
+  Qed.
+      
+  Program Definition map : list V := map_rec l.
     
 End Map_DependentRecursor.