Stop using [obligation_tactic] from Program.Tactics as the default

obligation tactic so that [Program] can work without importing 
anything.


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

8 files changed, 53 insertions, 37 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 071ffb2c5a..a1cbeb710a 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -151,9 +151,7 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ 
-    Coqlib.check_required_library ["Coq";"Program";"Tactics"];
-    Tacinterp.add_tacdef false 
-      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ]
+    Subtac_obligations.set_default_tactic (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 c4efef11b1..c0de6478a4 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -112,6 +112,8 @@ module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
 
 let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
 
+let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
+
 let map_cardinal m = 
   let i = ref 0 in 
     ProgMap.iter (fun _ _ -> incr i) m;
@@ -130,7 +132,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
+  from_prg := ProgMap.empty; set_default_tactic (Tacexpr.TacId [])
 
 (** Beware: if this code is dynamically loaded via dynlink after the start
     of Coq, then this [init] function will not be run by [Lib.init ()].
@@ -150,16 +152,35 @@ let cache (_, (infos, tac)) =
   from_prg := infos;
   set_default_tactic tac
 
+let load (_, (_, tac)) =
+  set_default_tactic tac
+
+let subst (_, s, (infos, tac)) = 
+  (infos, Tacinterp.subst_tactic s tac)
+
 let (input,output) = 
   declare_object
     { (default_object "Program state") with
       cache_function = cache;
-      load_function = (fun _ -> cache);
-      open_function = (fun _ -> cache);
-      classify_function = (fun _ -> Dispose);
+      load_function = (fun _ -> load);
+      open_function = (fun _ -> load);
+      classify_function = (fun (infos, tac) ->
+	if not (ProgMap.is_empty infos) then
+	  errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
+				   prlist_with_sep spc (fun x -> Nameops.pr_id x)
+				   (map_keys infos));
+	Substitute (ProgMap.empty, tac));
+      subst_function = subst;
       export_function = (fun x -> Some x) }
+
+let update_state () = 
+(*   msgnl (str "Updating obligations info"); *)
+  Lib.add_anonymous_leaf (input (!from_prg, !default_tactic_expr))
     
 open Evd
+
+let progmap_remove prg = 
+  from_prg := ProgMap.remove prg.prg_name !from_prg
 	  
 let rec intset_to = function
     -1 -> Intset.empty
@@ -195,6 +216,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 ();
           VarRef prg.prg_name
     | (Global|Local) ->
 	let c =
@@ -206,6 +228,7 @@ let declare_definition prg =
 	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
 	  print_message (Subtac_utils.definition_message prg.prg_name);
 	  prg.prg_hook local gr;
+	  progmap_remove prg; update_state ();
 	  gr
 
 open Pp
@@ -267,7 +290,9 @@ let declare_mutual_definition l =
     Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      first.prg_hook local gr; kn
+      first.prg_hook local gr; 
+      List.iter progmap_remove l;
+      update_state (); kn
       
 let declare_obligation obl body =
   match obl.obl_status with
@@ -320,11 +345,7 @@ let get_prog_err n =
   try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
 
 let obligations_solved prg = (snd prg.prg_obligations) = 0
-
-let update_state s = 
-(*   msgnl (str "Updating obligations info"); *)
-  Lib.add_anonymous_leaf (input s)
-
+    
 type progress = 
     | Remain of int 
     | Dependent
@@ -343,25 +364,19 @@ 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;
     obligations_message rem;
-    let res = 
-      if rem > 0 then Remain rem
-      else (
-	match prg'.prg_deps with
-	| [] ->
-	    let kn = declare_definition prg' in
-	      from_prg := ProgMap.remove prg.prg_name !from_prg;
-	      Defined kn
-	| 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 
-		(let kn = declare_mutual_definition progs in
-		   from_prg := List.fold_left
-		     (fun acc x -> 
-		       ProgMap.remove x.prg_name acc) !from_prg progs;
-		  Defined (ConstRef kn))
-	      else Dependent);
-    in update_state (!from_prg, !default_tactic_expr); res
-  
+    if rem > 0 then Remain rem
+    else (
+      match prg'.prg_deps with
+      | [] ->
+	  let kn = declare_definition prg' in
+	    Defined kn
+      | 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
+	      let kn = declare_mutual_definition progs in
+		Defined (ConstRef kn)
+	    else Dependent)
+    
 let is_defined obls x = obls.(x).obl_body <> None
 
 let deps_remaining obls deps = 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 100ddbe3ed..1d3edf1de5 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -21,6 +21,7 @@ Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Import Coq.Classes.Morphisms.
+Require Import Coq.Program.Tactics.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 1373e1952d..b672651b92 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -16,6 +16,8 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
+Obligation Tactic := simpl_relation.
+
 (** Standard instances for [not], [iff] and [impl]. *)
 
 (** Logical negation. *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index edfd1094d9..5c65244814 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -130,7 +130,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligation_tactic ::= simpl_relation.
+Obligation Tactic := simpl_relation.
 
 (** Logical implication. *)
 
@@ -412,4 +412,4 @@ Instance: RewriteRelation (@relation_equivalence A).
 (** Any [Equivalence] declared in the context is automatically considered 
    a rewrite relation. *)
 
-Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
\ No newline at end of file
+Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 063b429285..055f02f8b9 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -136,4 +136,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
-Ltac obligation_tactic ::= program_simpl.
+Obligation Tactic := program_simpl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index d009a456ed..f58f227e54 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -173,4 +173,4 @@ Ltac default_add_morphism_tactic :=
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
 
-Ltac obligation_tactic ::= program_simpl.
+Obligation Tactic := program_simpl.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 09f0f5ba03..7e8fedceb7 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -291,4 +291,4 @@ Ltac program_simplify :=
 
 Ltac program_simpl := program_simplify ; auto.
 
-Ltac obligation_tactic := program_simpl.
+Obligation Tactic := program_simpl.