diff options
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 30 |
1 files changed, 26 insertions, 4 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index b56ecc3d..243cb191 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 8917 2006-06-07 16:59:05Z herbelin $ *) +(* $Id: g_subtac.ml4 9326 2006-10-31 12:57:26Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) @@ -30,6 +30,7 @@ open Topconstr module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic module SubtacGram = struct @@ -40,15 +41,31 @@ end open SubtacGram open Util +open Pcoq + +let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc; + GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g ] ] ; + + Constr.binder_let: + [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in + LocalRawAssum ([id], typ) + ] ]; + + Constr.binder: + [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in + ([id], typ) ] ]; + END + 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), @@ -57,6 +74,11 @@ let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_arg Genarg.create_arg "subtac_gallina_loc" VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> - [ Subtac.subtac g ] +[ "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) ] +| [ "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) ] +| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] +| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] END |