diff options
| author | letouzey | 2012-04-26 09:54:18 +0000 |
|---|---|---|
| committer | letouzey | 2012-04-26 09:54:18 +0000 |
| commit | 845d6f167a0b2f31bd77cd98de0522873c0683a7 (patch) | |
| tree | c58041ec79507291d986e95d8c8b107984b486e7 | |
| parent | 47c1c7976a6830227edd8e125f6993ae4e15f6a6 (diff) | |
migrate g_obligations.ml4 in parsing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 7f5991d385..f86fd0fecd 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 eed6caea30..6ccbdb7523 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 b46d8fa8a3..d242036f7f 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -18,7 +18,6 @@ Backtrack Vernacinterp Mltop Vernacentries -G_obligations Whelp Vernac Ide_slave |