aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml44
-rw-r--r--intf/tacexpr.mli1
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--printing/pptactic.ml4
-rw-r--r--tactics/coretactics.ml420
-rw-r--r--tactics/tacintern.ml1
-rw-r--r--tactics/tacinterp.ml9
-rw-r--r--tactics/tacsubst.ml1
-rw-r--r--tactics/tauto.ml416
-rw-r--r--theories/Init/Notations.v10
10 files changed, 31 insertions, 39 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 32001e629..67331727a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -390,10 +390,6 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacSplit (ev,l) ->
<:expr< Tacexpr.TacSplit
($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>>
- | Tacexpr.TacConstructor (ev,n,l) ->
- let n = mlexpr_of_or_var mlexpr_of_int n in
- <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
-
(* Conversion *)
| Tacexpr.TacReduce (r,cl) ->
let l = mlexpr_of_clause cl in
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3b5868e9e..88e5c3696 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -149,7 +149,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
(* Trmuctors *)
| TacSplit of evars_flag * 'trm bindings list
- | TacConstructor of evars_flag * int or_var * 'trm bindings
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c32ade38c..b9eaf53ee 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -645,10 +645,6 @@ GEXTEND Gram
| "exists"; bll = opt_bindings -> TacSplit (false,bll)
| IDENT "eexists"; bll = opt_bindings ->
TacSplit (true,bll)
- | IDENT "constructor"; n = nat_or_var; l = with_bindings ->
- TacConstructor (false,n,l)
- | IDENT "econstructor"; n = nat_or_var; l = with_bindings ->
- TacConstructor (true,n,l)
(* Equivalence relations *)
| IDENT "symmetry"; "in"; cl = in_clause -> TacSymmetry cl
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 24f374b17..cdcff9bb2 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -778,10 +778,6 @@ and pr_atom1 = function
(* Constructors *)
| TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
- | TacConstructor (ev,n,l) ->
- hov 1 (str (with_evars ev "constructor") ++
- pr_or_var pr_intarg n ++ pr_bindings l)
-
(* Conversion *)
| TacReduce (r,h) ->
hov 1 (pr_red_expr r ++
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 731c6df06..196507274 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -106,10 +106,30 @@ END
TACTIC EXTEND constructor
[ "constructor" ] -> [ Tactics.any_constructor false None ]
+| [ "constructor" int_or_var(i) ] -> [
+ let i = Tacinterp.interp_int_or_var ist i in
+ Tactics.constructor_tac false None i NoBindings
+ ]
+| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
+ let { Evd.sigma = sigma; it = bl } = bl in
+ let i = Tacinterp.interp_int_or_var ist i in
+ let tac c = Tactics.constructor_tac false None i c in
+ Tacticals.New.tclWITHHOLES false tac sigma bl
+ ]
END
TACTIC EXTEND econstructor
[ "econstructor" ] -> [ Tactics.any_constructor true None ]
+| [ "econstructor" int_or_var(i) ] -> [
+ let i = Tacinterp.interp_int_or_var ist i in
+ Tactics.constructor_tac true None i NoBindings
+ ]
+| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
+ let { Evd.sigma = sigma; it = bl } = bl in
+ let i = Tacinterp.interp_int_or_var ist i in
+ let tac c = Tactics.constructor_tac true None i c in
+ Tacticals.New.tclWITHHOLES true tac sigma bl
+ ]
END
(** Specialize *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 197caf3bd..6c9e20289 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -523,7 +523,6 @@ let rec intern_atomic lf ist x =
(* Constructors *)
| TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
- | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
(* Conversion *)
| TacReduce (r,cl) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a393ea4f6..2bb8ab840 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1760,15 +1760,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
Tacticals.New.tclWITHHOLES ev (Tactics.split_with_bindings ev) sigma bll
end
- | TacConstructor (ev,n,bl) ->
- Proofview.Goal.raw_enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
- let sigma, bl = interp_bindings ist env sigma bl in
- Tacticals.New.tclWITHHOLES ev
- (Tactics.constructor_tac ev None (interp_int_or_var ist n)) sigma bl
- end
-
(* Conversion *)
| TacReduce (r,cl) ->
Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d0894d76f..d8ff931d3 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -181,7 +181,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Constructors *)
| TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)
- | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
(* Conversion *)
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bdacf85a8..4f0bc5848 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -153,6 +153,11 @@ let flatten_contravariant_conj flags ist =
(** Dealing with disjunction *)
+let constructor i =
+ let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
+ let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
+ Tacexpr.TacAtom (Loc.ghost, Tacexpr.TacExtend (Loc.ghost, name, [i]))
+
let is_disj flags ist =
let t = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary t) &&
@@ -176,12 +181,11 @@ let flatten_contravariant_disj flags ist =
let hyp = valueIn (Value.of_constr hyp) in
iter_tac (List.map_i (fun i arg ->
let typ = valueIn (Value.of_constr (mkArrow arg c)) in
- let i = Tacexpr.TacGeneric (in_gen (rawwit wit_int) i) in
+ let ci = constructor i in
<:tactic<
let typ := $typ in
let hyp := $hyp in
- let i := $i in
- assert typ by (intro; apply hyp; constructor i; assumption)
+ assert typ by (intro; apply hyp; $ci; assumption)
>>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
| _ ->
<:tactic<fail>>
@@ -199,9 +203,10 @@ let not_dep_intros ist =
let axioms flags ist =
let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
and t_is_empty = tacticIn is_empty in
+ let c1 = constructor 1 in
<:tactic<
match reverse goal with
- | |- ?X1 => $t_is_unit_or_eq; constructor 1
+ | |- ?X1 => $t_is_unit_or_eq; $c1
| _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
| _:?X1 |- ?X1 => assumption
end >>
@@ -214,6 +219,7 @@ let simplif flags ist =
and t_flatten_contravariant_disj = tacticIn (flatten_contravariant_disj flags)
and t_is_disj = tacticIn (is_disj flags)
and t_not_dep_intros = tacticIn not_dep_intros in
+ let c1 = constructor 1 in
<:tactic<
$t_not_dep_intros;
repeat
@@ -231,7 +237,7 @@ let simplif flags ist =
$t_is_unit_or_eq; cut X2;
[ intro; clear id
| (* id : forall (_: ?X1), ?X2 |- ?X2 *)
- cut X1; [exact id| constructor 1; fail]
+ cut X1; [exact id| $c1; fail]
]
| id: forall (_ : ?X1), ?X2|- _ =>
$t_flatten_contravariant_conj
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index fbad368c2..5095329cd 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -90,13 +90,3 @@ Declare ML Module "g_class".
Declare ML Module "g_eqdecide".
Declare ML Module "g_rewrite".
Declare ML Module "tauto".
-
-(** Small hack to overcome the fact that the (e)constructor tactics need to have
- a proper parsing rule, because the variants with arguments conflicts
- with it. *)
-Module CoreTactics.
-Declare ML Module "coretactics".
-End CoreTactics.
-
-Tactic Notation "constructor" := CoreTactics.constructor.
-Tactic Notation "econstructor" := CoreTactics.econstructor.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:51:43 +0000