diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /contrib/subtac/g_subtac.ml4 | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 88243b60..4cf5336d 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -14,7 +14,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *) open Flags @@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ Coqlib.check_required_library ["Coq";"Program";"Tactics"]; Tacinterp.add_tacdef false - [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations |