From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- contrib/subtac/g_subtac.ml4 | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'contrib/subtac/g_subtac.ml4') 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 -- cgit v1.2.3