aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/q_coqast.ml42
-rw-r--r--interp/constrarg.ml6
-rw-r--r--interp/constrarg.mli4
-rw-r--r--lib/genarg.ml6
-rw-r--r--lib/genarg.mli2
-rw-r--r--parsing/g_tactic.ml45
-rw-r--r--parsing/pcoq.ml44
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--printing/pptactic.ml6
-rw-r--r--tactics/extraargs.ml42
-rw-r--r--tactics/extratactics.ml421
-rw-r--r--tactics/extratactics.mli2
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml15
-rw-r--r--tactics/tacsubst.ml6
16 files changed, 47 insertions, 43 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index d884a10cb..dc521e20d 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -39,7 +39,7 @@ let rec make_wit loc = function
| ConstrArgType -> <:expr< Constrarg.wit_constr >>
| ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
| RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
- | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
+ | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
| ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
| BindingsArgType -> <:expr< Constrarg.wit_bindings >>
| ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 02c00e3f0..b405539ec 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -207,7 +207,7 @@ let rec mlexpr_of_argtype loc = function
| Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
- | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
+ | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
| Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
| Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
| Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 16af7c308..97004a93d 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -60,11 +60,7 @@ let wit_constr = unsafe_of_type ConstrArgType
let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
-let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b)
-
-let wit_open_constr = wit_open_constr_gen false
-
-let wit_casted_open_constr = wit_open_constr_gen true
+let wit_open_constr = unsafe_of_type OpenConstrArgType
let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1233e165f..b83c20065 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -57,12 +57,8 @@ val wit_constr_may_eval :
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
constr) genarg_type
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 98287d184..0f1e50568 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -20,7 +20,7 @@ type argument_type =
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | OpenConstrArgType of bool
+ | OpenConstrArgType
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
@@ -38,7 +38,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| ConstrArgType, ConstrArgType -> true
| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
| QuantHypArgType, QuantHypArgType -> true
-| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2
+| OpenConstrArgType, OpenConstrArgType -> true
| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
| BindingsArgType, BindingsArgType -> true
| RedExprArgType, RedExprArgType -> true
@@ -59,7 +59,7 @@ let rec pr_argument_type = function
| ConstrArgType -> str "constr"
| ConstrMayEvalArgType -> str "constr_may_eval"
| QuantHypArgType -> str "qhyp"
-| OpenConstrArgType _ -> str "open_constr"
+| OpenConstrArgType -> str "open_constr"
| ConstrWithBindingsArgType -> str "constr_with_bindings"
| BindingsArgType -> str "bindings"
| RedExprArgType -> str "redexp"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index e2654fcf5..3d5828bbb 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -199,7 +199,7 @@ type argument_type =
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | OpenConstrArgType of bool
+ | OpenConstrArgType
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index eb483c50c..93afb3d5a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -215,7 +215,7 @@ let merge_occurrences loc cl = function
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
- bindings red_expr int_or_var open_constr casted_open_constr
+ bindings red_expr int_or_var open_constr
simple_intropattern;
int_or_var:
@@ -236,9 +236,6 @@ GEXTEND Gram
open_constr:
[ [ c = constr -> ((),c) ] ]
;
- casted_open_constr:
- [ [ c = constr -> ((),c) ] ]
- ;
induction_arg:
[ [ n = natural -> ElimOnAnonHyp n
| c = constr_with_bindings -> induction_arg_of_constr c
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 79228e946..d25efa72a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -377,9 +377,7 @@ module Tactic =
(* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic (rawwit (wit_open_constr_gen false)) "open_constr"
- let casted_open_constr =
- make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr"
+ make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
let constr_with_bindings =
make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
let bindings =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index bbb71a170..56282f2f6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,7 +213,6 @@ module Tactic :
sig
open Glob_term
val open_constr : open_constr_expr Gram.entry
- val casted_open_constr : open_constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e1324c3ee..f091a2e1d 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -158,7 +158,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
(out_gen (rawwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (rawwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
| BindingsArgType ->
@@ -196,7 +196,7 @@ let rec pr_glb_generic prc prlc prtac prpat x =
pr_red_expr
(prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
(out_gen (glbwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (glbwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
| BindingsArgType ->
@@ -227,7 +227,7 @@ let rec pr_top_generic prc prlc prtac prpat x =
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
(out_gen (topwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (topwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
pr_with_bindings prc prlc (c,b)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index ccc231cf2..a3c531f80 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -116,7 +116,7 @@ ARGUMENT EXTEND glob
GLOB_TYPED AS glob_constr_and_expr
GLOB_PRINTED BY pr_gen
- [ lconstr(c) ] -> [ c ]
+ [ constr(c) ] -> [ c ]
END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c81e7ce3f..18326435c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -324,8 +324,27 @@ END
let refine_tac = Tactics.New.refine
+let refine_red_flags =
+ Genredexpr.Lazy {
+ Genredexpr.rBeta=true;
+ rIota=true;
+ rZeta=false;
+ rDelta=false;
+ rConst=[];
+ }
+
+let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
+
+let refine_tac (ist, c) =
+ let c = Goal.Refinable.make begin fun h ->
+ Goal.Refinable.constr_of_raw h true true c
+ end in
+ Proofview.Goal.lift c >>= fun c ->
+ Proofview.tclSENSITIVE (Goal.refine c) <*>
+ Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+
TACTIC EXTEND refine
- [ "refine" casted_open_constr(c) ] -> [ refine_tac c ]
+ [ "refine" glob(c) ] -> [ refine_tac c ]
END
(**********************************************************************)
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 7a0fabe1f..2b28a6547 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,6 +11,6 @@ open Proof_type
val discrHyp : Names.Id.t -> unit Proofview.tactic
val injHyp : Names.Id.t -> unit Proofview.tactic
-val refine_tac : Evd.open_constr -> unit Proofview.tactic
+(* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 261e8583e..19ab65d22 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -736,9 +736,9 @@ and intern_genarg ist x =
(intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x))
| RedExprArgType ->
in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x))
- | OpenConstrArgType b ->
- in_gen (glbwit (wit_open_constr_gen b))
- ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x)))
+ | OpenConstrArgType ->
+ in_gen (glbwit wit_open_constr)
+ ((),intern_constr ist (snd (out_gen (rawwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (glbwit wit_constr_with_bindings)
(intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0821423b5..ce216b15d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -144,7 +144,7 @@ let pr_inspect env expr result =
let pp_result =
if has_type result (topwit wit_tacvalue) then
match to_tacvalue result with
- | VRTactic _ -> str "a VRTactic"
+ | VRTactic -> str "a VRTactic"
| VFun (_, il, ul, b) ->
let pp_body = Pptactic.pr_glob_tactic env b in
let pr_sep () = str ", " in
@@ -1346,13 +1346,12 @@ and interp_genarg ist env sigma concl gl x =
in
evdref := sigma;
in_gen (topwit wit_red_expr) r_interp
- | OpenConstrArgType casted ->
- let expected_type =
- if casted then OfType concl else WithoutTypeConstraint in
- in_gen (topwit (wit_open_constr_gen casted))
+ | OpenConstrArgType ->
+ let expected_type = WithoutTypeConstraint in
+ in_gen (topwit wit_open_constr)
(interp_open_constr ~expected_type
ist env !evdref
- (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
+ (snd (out_gen (glbwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (topwit wit_constr_with_bindings)
(pack_sigma (interp_constr_with_bindings ist env !evdref
@@ -1983,7 +1982,7 @@ and interp_atomic ist tac =
Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
(Proofview.V82.tclEVARS sigma) <*>
(Proofview.Goal.return v)
- | OpenConstrArgType false ->
+ | OpenConstrArgType ->
Proofview.Goal.return (
Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
(Proofview.V82.tclEVARS sigma) <*>
@@ -2043,7 +2042,7 @@ and interp_atomic ist tac =
Proofview.V82.tactic (tclEVARS newsigma) <*>
Proofview.Goal.return v
| QuantHypArgType | RedExprArgType
- | OpenConstrArgType _ | ConstrWithBindingsArgType
+ | ConstrWithBindingsArgType
| BindingsArgType
| OptArgType _ | PairArgType _
-> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations."))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7491c9a8f..57aa88368 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -312,9 +312,9 @@ and subst_genarg subst (x:glob_generic_argument) =
(out_gen (glbwit wit_quant_hyp) x))
| RedExprArgType ->
in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x))
- | OpenConstrArgType b ->
- in_gen (glbwit (wit_open_constr_gen b))
- ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x)))
+ | OpenConstrArgType ->
+ in_gen (glbwit wit_open_constr)
+ ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (glbwit wit_constr_with_bindings)
(subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 15:34:45 +0000