diff options
| -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" |