diff options
| -rw-r--r-- | parsing/g_obligations.ml4 (renamed from toplevel/g_obligations.ml4) | 15 | ||||
| -rw-r--r-- | parsing/highparsing.mllib | 1 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 1 |
3 files changed, 8 insertions, 9 deletions
diff --git a/toplevel/g_obligations.ml4 b/parsing/g_obligations.ml4 index 7f5991d38..f86fd0fec 100644 --- a/toplevel/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -17,7 +17,6 @@ open Flags open Util open Names open Nameops -open Vernacentries open Reduction open Term open Libnames @@ -61,7 +60,7 @@ GEXTEND Gram let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in [LocalRawAssum ([id], default_binder_kind, typ)] ] ]; - + END type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type @@ -74,15 +73,15 @@ let (wit_withtac : Genarg.tlevel withtac_argtype), open Obligations VERNAC COMMAND EXTEND Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> +| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" integer(num) withtac(tac) ] -> [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> [ next_obligation (Some name) tac ] | [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] END @@ -117,7 +116,7 @@ VERNAC COMMAND EXTEND Admit_Obligations VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic + set_default_tactic (Vernacexpr.use_section_locality ()) (Tacinterp.glob_tactic t) ] END diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index eed6caea3..6ccbdb752 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,3 +4,4 @@ G_prim G_proofs G_tactic G_ltac +G_obligations
\ No newline at end of file diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index b46d8fa8a..d242036f7 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,6 @@ Backtrack Vernacinterp Mltop Vernacentries -G_obligations Whelp Vernac Ide_slave |