Support "Local Obligation Tactic" (now the default in sections).

Update Numbers that was implicitely using [simpl_relation] instead of
the default tactic [program_simpl].


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

3 files changed, 22 insertions, 21 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 098418a7e3..fe272edd50 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -151,7 +151,9 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
-    Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
+    Subtac_obligations.set_default_tactic 
+      (Vernacexpr.use_section_locality ())
+      (Tacinterp.glob_tactic t) ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 45dfc44bcb..e506e7e511 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -155,14 +155,14 @@ let _ =
 
 let progmap_union = ProgMap.fold ProgMap.add
 
-let cache (_, tac) =
+let cache (_, (local, tac)) =
   set_default_tactic tac
 
-let load (_, tac) =
-  set_default_tactic tac
+let load (_, (local, tac)) =
+  if not local then set_default_tactic tac
 
-let subst (s, tac) =
-  Tacinterp.subst_tactic s tac
+let subst (s, (local, tac)) =
+  (local, Tacinterp.subst_tactic s tac)
 
 let (input,output) =
   declare_object
@@ -170,19 +170,19 @@ let (input,output) =
       cache_function = cache;
       load_function = (fun _ -> load);
       open_function = (fun _ -> load);
-      classify_function = (fun tac ->
+      classify_function = (fun (local, tac) ->
 	if not (ProgMap.is_empty !from_prg) then
 	  errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
-				   prlist_with_sep spc (fun x -> Nameops.pr_id x)
-				   (map_keys !from_prg));
-	Substitute tac);
+				     prlist_with_sep spc (fun x -> Nameops.pr_id x)
+				     (map_keys !from_prg));
+	if local then Dispose else Substitute (local, tac));
       subst_function = subst}
+    
+let update_state local =
+  Lib.add_anonymous_leaf (input (local, !default_tactic_expr))
 
-let update_state () =
-  Lib.add_anonymous_leaf (input !default_tactic_expr)
-
-let set_default_tactic t =
-  set_default_tactic t; update_state ()
+let set_default_tactic local t =
+  set_default_tactic t; update_state local
 
 open Evd
 
@@ -223,7 +223,7 @@ let declare_definition prg =
             Flags.if_verbose msg_warning
 	      (str"Local definition " ++ Nameops.pr_id prg.prg_name ++
 		  str" is not visible from current goals");
-	  progmap_remove prg; update_state ();
+	  progmap_remove prg; 
           VarRef prg.prg_name
     | (Global|Local) ->
 	let c =
@@ -234,7 +234,7 @@ let declare_definition prg =
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
 	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
 	  print_message (Subtac_utils.definition_message prg.prg_name);
-	  progmap_remove prg; update_state ();
+	  progmap_remove prg; 
 	  prg.prg_hook local gr;
 	  gr
 
@@ -297,8 +297,7 @@ let declare_mutual_definition l =
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
       first.prg_hook local gr;
-      List.iter progmap_remove l;
-      update_state (); kn
+      List.iter progmap_remove l; kn
       
 let declare_obligation prg obl body =
   let body = reduce body in
@@ -383,7 +382,7 @@ let obligations_message rem =
 
 let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
-    from_prg := map_replace prg.prg_name prg' !from_prg; update_state ();
+    from_prg := map_replace prg.prg_name prg' !from_prg; 
     obligations_message rem;
     if rem > 0 then Remain rem
     else (
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 2666430a8f..d32653b095 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -15,7 +15,7 @@ type progress = (* Resolution status of a program *)
   | Dependent (* Dependent on other definitions *)
   | Defined of global_reference (* Defined as id *)
       
-val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
+val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
 val default_tactic : unit -> Proof_type.tactic
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)