aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml479
-rw-r--r--plugins/ltac/g_ltac.ml43
-rw-r--r--plugins/ltac/rewrite.ml5
-rw-r--r--plugins/ltac/taccoerce.ml18
-rw-r--r--plugins/ltac/taccoerce.mli3
-rw-r--r--plugins/ltac/tacinterp.ml13
6 files changed, 52 insertions, 69 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 982fc7cc3c..3e3965b94a 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -25,6 +25,7 @@ open Termops
open Equality
open Misctypes
open Proofview.Notations
+open Vernacinterp
DECLARE PLUGIN "ltac_plugin"
@@ -249,11 +250,10 @@ TACTIC EXTEND rewrite_star
(**********************************************************************)
(* Hint Rewrite *)
-let add_rewrite_hint bases ort t lcsr =
+let add_rewrite_hint ~poly bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
- let poly = Flags.use_polymorphic_flag () in
- let f ce =
+ let f ce =
let c, ctx = Constrintern.interp_constr env sigma ce in
let ctx =
let ctx = UState.context_set ctx in
@@ -270,16 +270,16 @@ let add_rewrite_hint bases ort t lcsr =
let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
-VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint
+VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
[ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o None l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- [ add_rewrite_hint bl o (Some t) l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- [ add_rewrite_hint ["core"] o None l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- [ add_rewrite_hint ["core"] o (Some t) l ]
+ [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ]
END
(**********************************************************************)
@@ -290,7 +290,7 @@ open EConstr
open Vars
open Coqlib
-let project_hint pri l2r r =
+let project_hint ~poly pri l2r r =
let gr = Smartlocate.global_with_alias r in
let env = Global.env() in
let sigma = Evd.from_env env in
@@ -313,30 +313,28 @@ let project_hint pri l2r r =
let id =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
- let poly = Flags.use_polymorphic_flag () in
let ctx = Evd.const_univ_entry ~poly sigma in
let c = EConstr.to_constr sigma c in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
(info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
-let add_hints_iff ?locality l2r lc n bl =
- Hints.add_hints (Locality.make_module_locality locality) bl
- (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
+let add_hints_iff ~atts l2r lc n bl =
+ let open Vernacinterp in
+ Hints.add_hints (Locality.make_module_locality atts.locality) bl
+ (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality true lc n bl;
+ add_hints_iff ~atts true lc n bl;
st
end
]
| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality true lc n ["core"];
+ add_hints_iff ~atts true lc n ["core"];
st
end
]
@@ -346,15 +344,13 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality false lc n bl;
+ add_hints_iff ~atts false lc n bl;
st
end
]
| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
[ fun ~atts ~st -> begin
- let open Vernacinterp in
- add_hints_iff ?locality:atts.locality false lc n ["core"];
+ add_hints_iff ~atts false lc n ["core"];
st
end
]
@@ -430,34 +426,46 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
| [ "Type" ] -> [ InType ]
END*)
-VERNAC COMMAND EXTEND DeriveInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ]
| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion
| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s false inv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ]
| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
- -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveDependentInversion
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion
| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s true dinv_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ]
END
-VERNAC COMMAND EXTEND DeriveDependentInversionClear
+VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear
| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
=> [ seff na ]
- -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ]
END
(**********************************************************************)
@@ -1117,3 +1125,12 @@ VERNAC COMMAND EXTEND OptimizeProof
| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] ->
[ Gc.compact () ]
END
+
+(** tactic analogous to "OPTIMIZE HEAP" *)
+
+let tclOPTIMIZE_HEAP =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))
+
+TACTIC EXTEND optimize_heap
+| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ]
+END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ebf6e450b1..cc7ce339b2 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -327,7 +327,8 @@ GEXTEND Gram
| IDENT "all"; ":" -> SelectAll ] ]
;
tactic_mode:
- [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ]
+ [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g
+ | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ]
;
command:
[ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a698b05dd7..3cbb110010 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n =
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
- poly (ConstRef cst));
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
else
let kind = Decl_kinds.Global, poly,
@@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n =
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
- glob poly (ConstRef cst));
+ glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9ae112d371..e5933de2a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -61,12 +61,9 @@ struct
type t = Val.t
-let normalize v = v
-
let of_constr c = in_gen (topwit wit_constr) c
let to_constr v =
- let v = normalize v in
if has_type v (topwit wit_constr) then
let c = out_gen (topwit wit_constr) v in
Some c
@@ -78,7 +75,6 @@ let to_constr v =
let of_uconstr c = in_gen (topwit wit_uconstr) c
let to_uconstr v =
- let v = normalize v in
if has_type v (topwit wit_uconstr) then
Some (out_gen (topwit wit_uconstr) v)
else None
@@ -86,7 +82,6 @@ let to_uconstr v =
let of_int i = in_gen (topwit wit_int) i
let to_int v =
- let v = normalize v in
if has_type v (topwit wit_int) then
Some (out_gen (topwit wit_int) v)
else None
@@ -108,14 +103,12 @@ let constr_of_id env id =
(* Gives the constr corresponding to a Constr_context tactic_arg *)
let coerce_to_constr_context v =
- let v = Value.normalize v in
if has_type v (topwit wit_constr_context) then
out_gen (topwit wit_constr_context) v
else raise (CannotCoerceTo "a term context")
(* Interprets an identifier which must be fresh *)
let coerce_var_to_ident fresh env sigma v =
- let v = Value.normalize v in
let fail () = raise (CannotCoerceTo "a fresh identifier") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
@@ -140,7 +133,6 @@ let g = sigma in
let id_of_name = function
| Name.Anonymous -> Id.of_string "x"
| Name.Name x -> x in
- let v = Value.normalize v in
let fail () = raise (CannotCoerceTo "an identifier") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
@@ -179,7 +171,6 @@ let id_of_name = function
let coerce_to_intro_pattern env sigma v =
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
snd (out_gen (topwit wit_intro_pattern) v)
else if has_type v (topwit wit_var) then
@@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v =
| _ -> raise (CannotCoerceTo "a naming introduction pattern")
let coerce_to_hint_base v =
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
| _, IntroNaming (IntroIdentifier id) -> Id.to_string id
@@ -206,13 +196,11 @@ let coerce_to_hint_base v =
else raise (CannotCoerceTo "a hint base name")
let coerce_to_int v =
- let v = Value.normalize v in
if has_type v (topwit wit_int) then
out_gen (topwit wit_int) v
else raise (CannotCoerceTo "an integer")
let coerce_to_constr env v =
- let v = Value.normalize v in
let fail () = raise (CannotCoerceTo "a term") in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
@@ -230,7 +218,6 @@ let coerce_to_constr env v =
else fail ()
let coerce_to_uconstr env v =
- let v = Value.normalize v in
if has_type v (topwit wit_uconstr) then
out_gen (topwit wit_uconstr) v
else
@@ -243,7 +230,6 @@ let coerce_to_closed_constr env v =
let coerce_to_evaluable_ref env sigma v =
let fail () = raise (CannotCoerceTo "an evaluable reference") in
- let v = Value.normalize v in
let ev =
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
@@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v =
let coerce_to_hyp env sigma v =
let fail () = raise (CannotCoerceTo "a variable") in
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
| _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
@@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v =
(* Interprets a qualified name *)
let coerce_to_reference env sigma v =
- let v = Value.normalize v in
match Value.to_constr v with
| Some c ->
begin
@@ -318,7 +302,6 @@ let coerce_to_reference env sigma v =
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_quantified_hypothesis sigma v =
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
@@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v =
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_decl_or_quant_hyp env sigma v =
- let v = Value.normalize v in
if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
else
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index d7b253a687..dce16b7333 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -31,9 +31,6 @@ module Value :
sig
type t = Val.t
- val normalize : t -> t
- (** Eliminated the leading dynamic type casts. *)
-
val of_constr : constr -> t
val to_constr : t -> constr option
val of_uconstr : Ltac_pretype.closed_glob_constr -> t
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ccded44179..f2720954d0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v
(** More naming applications *)
let name_vfun appl vle =
- let vle = Value.normalize vle in
if has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
@@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
(* Displays a value *)
let pr_value env v =
- let v = Value.normalize v in
let pr_with_env pr =
match env with
| Some (env,sigma) -> pr env sigma
@@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with
| Some trace -> Proofview.tclUNIT (call :: trace)
let propagate_trace ist loc id v =
- let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
@@ -298,7 +295,6 @@ let propagate_trace ist loc id v =
else Proofview.tclUNIT v
let append_trace trace v =
- let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
match to_tacvalue v with
| VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b))
@@ -307,11 +303,9 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
- let v = Value.normalize v in
let fail () = user_err ?loc
(str "Variable " ++ Id.print id ++ str " should be bound to a tactic.")
in
- let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
@@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with
let extract_ids ids lfun accu =
let fold id v accu =
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
if Id.List.mem id ids then accu
@@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c =
(** TODO: should use dedicated printers *)
let message_of_value v =
- let v = Value.normalize v in
let pr_with_env pr =
Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
let open Genprint in
@@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg =
try
(** FIXME: should be moved to taccoerce *)
let v = Id.Map.find id ist.lfun in
- let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
@@ -1248,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Ftactic.run args tac
and force_vrec ist v : Val.t Ftactic.t =
- let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
let v = to_tacvalue v in
match v with
@@ -1324,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
and interp_app loc ist fv largs : Val.t Ftactic.t =
let (>>=) = Ftactic.bind in
let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
- let fv = Value.normalize fv in
if has_type fv (topwit wit_tacvalue) then
match to_tacvalue fv with
(* if var=[] and body has been delayed by val_interp, then body
@@ -1377,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
(* Gives the tactic corresponding to the tactic value *)
and tactic_of_value ist vle =
- let vle = Value.normalize vle in
if has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl,trace,lfun,[],t) ->
@@ -1604,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
- let result = Value.normalize result in
try
let cresult = coerce_to_closed_constr env result in
Proofview.tclLIFT begin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:14:09 +0000