diff options
| author | msozeau | 2008-01-30 04:18:32 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-30 04:18:32 +0000 |
| commit | bf4ea1d3edb56f9f63da38d08dd9fc14f5f9a4a3 (patch) | |
| tree | 87fc096a8bfc8fa7da4d99df3c9c96c4cdedbfdf | |
| parent | 5eca868248b8faf8af73bd3bc015dea00a674752 (diff) | |
Use new redefinition support for the default obligations tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10485 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 2de804aa13..51e1a1709d 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -139,7 +139,9 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Tacinterp.add_tacdef false [((dummy_loc, id_of_string "program_simpl"), true, t)] ] +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ + Subtac.require_library "Coq.Program.Tactics"; + Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index c184169ac7..05bebf0f56 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -97,7 +97,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 "program_simpl" []) + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" []) let _ = Summary.declare_summary "program-tcc-table" |