summaryrefslogtreecommitdiff
path: root/contrib/subtac/g_subtac.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /contrib/subtac/g_subtac.ml4
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
-rw-r--r--contrib/subtac/g_subtac.ml450
1 files changed, 32 insertions, 18 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 43a3bec4..88243b60 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -6,15 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
+
+
(*
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *)
-(*i camlp4deps: "parsing/grammar.cma" i*)
-open Options
+open Flags
open Util
open Names
open Nameops
@@ -41,17 +44,20 @@ struct
let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
end
+open Rawterm
open SubtacGram
open Util
open Pcoq
-
+open Prim
+open Constr
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 subtac_nameopt;
+ GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt;
subtac_gallina_loc:
- [ [ g = Vernac.gallina -> loc, g ] ]
+ [ [ g = Vernac.gallina -> loc, g
+ | g = Vernac.gallina_ext -> loc, g ] ]
;
subtac_nameopt:
@@ -60,31 +66,31 @@ GEXTEND Gram
;
Constr.binder_let:
- [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
- let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
- LocalRawAssum ([id], typ)
+ [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
+ let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+ [LocalRawAssum ([id], default_binder_kind, typ)]
] ];
Constr.binder:
[ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+ ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)]))
| "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
- ([id],c)
+ ([id],default_binder_kind, c)
| "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
- (id::lid,c)
+ (id::lid,default_binder_kind, c)
] ];
END
-type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
+type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) 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),
- (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) =
+let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
+ (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype),
+ (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
Genarg.create_arg "subtac_gallina_loc"
-type 'a nameopt_argtype = (identifier option, 'a, 'a) Genarg.abstract_argument_type
+type 'a nameopt_argtype = (identifier option, 'a) Genarg.abstract_argument_type
let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype),
(globwit_subtac_nameopt : Genarg.glevel nameopt_argtype),
@@ -133,10 +139,18 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
END
VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [
+ Coqlib.check_required_library ["Coq";"Program";"Tactics"];
+ Tacinterp.add_tacdef false
+ [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, 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
+
+VERNAC COMMAND EXTEND Subtac_Show_Preterm
+| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ]
+| [ "Preterm" ] -> [ Subtac_obligations.show_term None ]
+END