Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

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