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