diff options
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 4cf5336d..7194d435 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 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: g_subtac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) open Flags @@ -112,25 +112,25 @@ END VERNAC COMMAND EXTEND Subtac_Solve_Obligation | [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ] END VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" ] -> - [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ] + [ Subtac_obligations.try_solve_obligations None None ] END VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations | [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ] + [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ] | [ "Solve" "All" "Obligations" ] -> - [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ] + [ Subtac_obligations.solve_all_obligations None ] END VERNAC COMMAND EXTEND Subtac_Admit_Obligations |