summaryrefslogtreecommitdiff
path: root/contrib/subtac/g_subtac.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /contrib/subtac/g_subtac.ml4
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
-rw-r--r--contrib/subtac/g_subtac.ml451
1 files changed, 44 insertions, 7 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 243cb191..e31326e9 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -10,7 +10,7 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 9326 2006-10-31 12:57:26Z msozeau $ *)
+(* $Id: g_subtac.ml4 9588 2007-02-02 16:17:13Z herbelin $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
@@ -37,6 +37,8 @@ struct
let gec s = Gram.Entry.create ("Subtac."^s)
(* types *)
let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+
+ let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
end
open SubtacGram
@@ -46,12 +48,17 @@ open Pcoq
let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder;
+ GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt;
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g ] ]
;
+ subtac_nameopt:
+ [ [ "ofb"; id=Prim.ident -> Some (id)
+ | -> None ] ]
+ ;
+
Constr.binder_let:
[ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
@@ -60,8 +67,12 @@ GEXTEND Gram
Constr.binder:
[ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
- ([id], typ) ] ];
+ ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+ | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
+ ([id],c)
+ | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
+ (id::lid,c)
+ ] ];
END
@@ -69,16 +80,42 @@ GEXTEND Gram
type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
- (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) gallina_loc_argtype),
+ (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr ) gallina_loc_argtype),
(rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) =
Genarg.create_arg "subtac_gallina_loc"
+type 'a nameopt_argtype = (identifier option, 'a, 'a) Genarg.abstract_argument_type
+
+let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype),
+ (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype),
+ (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) =
+ Genarg.create_arg "subtac_nameopt"
+
VERNAC COMMAND EXTEND Subtac
[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
-| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ]
-| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ]
+ END
+
+VERNAC COMMAND EXTEND Subtac_Obligations
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]
+| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]
+| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ]
+| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
+END
+
+VERNAC COMMAND EXTEND Subtac_Solve_Obligations
| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ]
+| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ]
+ END
+
+VERNAC COMMAND EXTEND Subtac_Set_Solver
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ]
+END
+
+VERNAC COMMAND EXTEND Subtac_Show_Obligations
| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
END