aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml21
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--parsing/g_tacticnew.ml44
-rw-r--r--parsing/pptactic.ml4
-rw-r--r--parsing/q_coqast.ml44
-rw-r--r--proofs/tacexpr.ml8
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/inv.ml12
-rw-r--r--tactics/inv.mli10
-rw-r--r--tactics/tacinterp.ml16
-rw-r--r--tactics/tacticals.ml14
-rw-r--r--tactics/tacticals.mli8
-rw-r--r--tactics/tactics.ml2
-rw-r--r--tactics/tactics.mli4
-rw-r--r--translate/pptacticnew.ml10
15 files changed, 58 insertions, 67 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f5507e722..3f3f8c4d2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -696,16 +696,9 @@ let xlate_lettac_clauses = function
CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res)
| None -> CT_unfold_list res;;
-let xlate_intro_patt_list = function
- [] -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
- | (fp::ll) ->
- CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT
- (CT_disj_pattern
- (CT_intro_patt_list(List.map xlate_intro_pattern fp),
- List.map
- (fun l ->
- CT_intro_patt_list(List.map xlate_intro_pattern l))
- ll));;
+let xlate_intro_patt_opt = function
+ None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+ | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
function
@@ -1155,12 +1148,12 @@ and xlate_tac =
| (*For translating tactics/Inv.v *)
TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
- xlate_intro_patt_list l,
+ xlate_intro_patt_opt l,
CT_id_list (List.map xlate_hyp idl))
| TacInversion (DepInversion (k,copt,l),quant_hyp) ->
let id = xlate_quantified_hypothesis quant_hyp in
CT_depinversion (compute_INV_TYPE k, id,
- xlate_intro_patt_list l, xlate_formula_opt copt)
+ xlate_intro_patt_opt l, xlate_formula_opt copt)
| TacInversion (InversionUsing (c,idlist), id) ->
let id = xlate_quantified_hypothesis id in
CT_use_inversion (id, xlate_formula c,
@@ -1174,11 +1167,11 @@ and xlate_tac =
| TacNewDestruct(a,b,(c,_)) ->
CT_new_destruct
(xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_list c)
+ xlate_intro_patt_opt c)
| TacNewInduction(a,b,(c,_)) ->
CT_new_induction
(xlate_int_or_constr a, xlate_using b,
- xlate_intro_patt_list c)
+ xlate_intro_patt_opt c)
| TacInstantiate (a, b, cl) ->
CT_instantiate(CT_int a, xlate_formula b,
xlate_clause cl)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 73718c629..ae9fc2aed 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -255,9 +255,7 @@ GEXTEND Gram
[ [ "using"; el = constr_with_bindings -> el ] ]
;
with_names:
- [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
- | "as"; "("; ids = LIST1 simple_intropattern SEP ","; ")" -> [ids]
- | -> [] ] ]
+ [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ]
;
simple_tactic:
[ [
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 721697c9a..e307f96f9 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -298,9 +298,7 @@ GEXTEND Gram
[ [ "using"; el = constr_with_bindings -> el ] ]
;
with_names:
- [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids
- | "as"; "("; ids = LIST1 simple_intropattern SEP ","; ")" -> [ids]
- | -> [] ] ]
+ [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ]
;
simple_tactic:
[ [
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9c27cb65b..67033d008 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -141,8 +141,8 @@ let pr_with_constr prc = function
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
let pr_with_names = function
- | [] -> mt ()
- | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
+ | None -> mt ()
+ | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
let pr_hyp_location pr_id = function
| id, _, (InHyp,_) -> spc () ++ pr_id id
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 87eb0784f..9813b3774 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -394,13 +394,13 @@ let rec mlexpr_of_atomic_tactic = function
<:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$,ref []) >>
| Tacexpr.TacNewInduction (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+ let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in
<:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref [])>>
| Tacexpr.TacSimpleDestruct h ->
<:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacNewDestruct (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
- let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) (fst ids) in
+ let ids = mlexpr_of_option mlexpr_of_intro_pattern (fst ids) in
<:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >>
(* Context management *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 062d415c3..1be84372c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -69,8 +69,8 @@ type inversion_kind =
| FullInversionClear
type ('c,'id) inversion_strength =
- | NonDepInversion of inversion_kind * 'id list * case_intro_pattern_expr
- | DepInversion of inversion_kind * 'c option * case_intro_pattern_expr
+ | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr option
+ | DepInversion of inversion_kind * 'c option * intro_pattern_expr option
| InversionUsing of 'c * 'id list
type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -132,10 +132,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Derived basic tactics *)
| TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)
| TacNewInduction of 'constr induction_arg * 'constr with_bindings option
- * (case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref)
+ * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
| TacSimpleDestruct of quantified_hypothesis
| TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
- * (case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref)
+ * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref)
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
| TacDecomposeAnd of 'constr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index cff5dccde..7c8c1b3c5 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -58,11 +58,11 @@ val h_simple_induction : quantified_hypothesis * (bool ref * intro_pattern_exp
val h_simple_destruct : quantified_hypothesis -> tactic
val h_new_induction :
constr induction_arg -> constr with_bindings option ->
- case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+ intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
val h_new_destruct :
constr induction_arg -> constr with_bindings option ->
- case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+ intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
val h_specialize : int option -> constr with_bindings -> tactic
val h_lapply : constr -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b9574db23..0810caa82 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -523,15 +523,15 @@ open Tacexpr
let inv k = inv_gen false k NoDep
-let half_inv_tac id = inv SimpleInversion [] (NamedHyp id)
-let inv_tac id = inv FullInversion [] (NamedHyp id)
-let inv_clear_tac id = inv FullInversionClear [] (NamedHyp id)
+let half_inv_tac id = inv SimpleInversion None (NamedHyp id)
+let inv_tac id = inv FullInversion None (NamedHyp id)
+let inv_clear_tac id = inv FullInversionClear None (NamedHyp id)
let dinv k c = inv_gen false k (Dep c)
-let half_dinv_tac id = dinv SimpleInversion None [] (NamedHyp id)
-let dinv_tac id = dinv FullInversion None [] (NamedHyp id)
-let dinv_clear_tac id = dinv FullInversionClear None [] (NamedHyp id)
+let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id)
+let dinv_tac id = dinv FullInversion None None (NamedHyp id)
+let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
(* InvIn will bring the specified clauses into the conclusion, and then
* perform inversion on the named hypothesis. After, it will intro them
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 4c3cb00f8..95bf4c6f7 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -21,19 +21,19 @@ type inversion_status = Dep of constr option | NoDep
val inv_gen :
bool -> inversion_kind -> inversion_status ->
- case_intro_pattern_expr -> quantified_hypothesis -> tactic
+ intro_pattern_expr option -> quantified_hypothesis -> tactic
val invIn_gen :
- inversion_kind -> case_intro_pattern_expr -> identifier list ->
+ inversion_kind -> intro_pattern_expr option -> identifier list ->
quantified_hypothesis -> tactic
val inv_clause :
- inversion_kind -> case_intro_pattern_expr -> identifier list ->
+ inversion_kind -> intro_pattern_expr option -> identifier list ->
quantified_hypothesis -> tactic
-val inv : inversion_kind -> case_intro_pattern_expr ->
+val inv : inversion_kind -> intro_pattern_expr option ->
quantified_hypothesis -> tactic
-val dinv : inversion_kind -> constr option -> case_intro_pattern_expr ->
+val dinv : inversion_kind -> constr option -> intro_pattern_expr option ->
quantified_hypothesis -> tactic
val half_inv_tac : identifier -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a0d791a58..4a08804c5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -549,10 +549,10 @@ let intern_redexp ist = function
let intern_inversion_strength lf ist = function
| NonDepInversion (k,idl,ids) ->
NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
- intern_case_intro_pattern lf ist ids)
+ option_app (intern_intro_pattern lf ist) ids)
| DepInversion (k,copt,ids) ->
DepInversion (k, option_app (intern_constr ist) copt,
- intern_case_intro_pattern lf ist ids)
+ option_app (intern_intro_pattern lf ist) ids)
| InversionUsing (c,idl) ->
InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
@@ -672,13 +672,13 @@ let rec intern_atomic lf ist x =
| TacNewInduction (c,cbo,(ids,ids')) ->
TacNewInduction (intern_induction_arg ist c,
option_app (intern_constr_with_bindings ist) cbo,
- (intern_case_intro_pattern lf ist ids,ids'))
+ (option_app (intern_intro_pattern lf ist) ids,ids'))
| TacSimpleDestruct h ->
TacSimpleDestruct (intern_quantified_hypothesis ist h)
| TacNewDestruct (c,cbo,(ids,ids')) ->
TacNewDestruct (intern_induction_arg ist c,
option_app (intern_constr_with_bindings ist) cbo,
- (intern_case_intro_pattern lf ist ids,ids'))
+ (option_app (intern_intro_pattern lf ist) ids,ids'))
| TacDoubleInduction (h1,h2) ->
let h1 = intern_quantified_hypothesis ist h1 in
let h2 = intern_quantified_hypothesis ist h2 in
@@ -1704,13 +1704,13 @@ and interp_atomic ist gl = function
| TacNewInduction (c,cbo,(ids,ids')) ->
h_new_induction (interp_induction_arg ist gl c)
(option_app (interp_constr_with_bindings ist gl) cbo)
- (interp_case_intro_pattern ist ids,ids')
+ (option_app (interp_intro_pattern ist) ids,ids')
| TacSimpleDestruct h ->
h_simple_destruct (interp_quantified_hypothesis ist gl h)
| TacNewDestruct (c,cbo,(ids,ids')) ->
h_new_destruct (interp_induction_arg ist gl c)
(option_app (interp_constr_with_bindings ist gl) cbo)
- (interp_case_intro_pattern ist ids,ids')
+ (option_app (interp_intro_pattern ist) ids,ids')
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist gl h1 in
let h2 = interp_quantified_hypothesis ist gl h2 in
@@ -1757,11 +1757,11 @@ and interp_atomic ist gl = function
(* Equality and inversion *)
| TacInversion (DepInversion (k,c,ids),hyp) ->
Inv.dinv k (option_app (pf_interp_constr ist gl) c)
- (interp_case_intro_pattern ist ids)
+ (option_app (interp_intro_pattern ist) ids)
(interp_quantified_hypothesis ist gl hyp)
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
Inv.inv_clause k
- (interp_case_intro_pattern ist ids)
+ (option_app (interp_intro_pattern ist) ids)
(List.map (interp_hyp ist gl) idl)
(interp_quantified_hypothesis ist gl hyp)
| TacInversion (InversionUsing (c,idl),hyp) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bd75581aa..7dc71ffc9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -267,11 +267,13 @@ type branch_assumptions = {
ba : branch_args; (* the branch args *)
assums : named_context} (* the list of assumptions introduced *)
-let compute_induction_names n names =
- let names = if names = [] then Array.make n [] else Array.of_list names in
- if Array.length names <> n then
- errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names");
- names
+let compute_induction_names n = function
+ | None ->
+ Array.make n []
+ | Some (IntroOrAndPattern names) when List.length names = n ->
+ Array.of_list names
+ | _ ->
+ errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
let compute_construtor_signatures isrec (_,k as ity) =
let rec analrec c recargs =
@@ -377,7 +379,7 @@ let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
let elim =
Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in
general_elim_then_using
- elim true [] tac predicate (indbindings,elimbindings) c gl
+ elim true None tac predicate (indbindings,elimbindings) c gl
let elimination_then tac = elimination_then_using tac None
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f6b6e5b00..1a6a540e6 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -129,13 +129,13 @@ type branch_assumptions = {
(* Useful for "as intro_pattern" modifier *)
val compute_induction_names :
- int -> case_intro_pattern_expr -> intro_pattern_expr list array
+ int -> intro_pattern_expr option -> intro_pattern_expr list array
val elimination_sort_of_goal : goal sigma -> sorts_family
val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family
val general_elim_then_using :
- constr -> (* isrec: *) bool -> case_intro_pattern_expr ->
+ constr -> (* isrec: *) bool -> intro_pattern_expr option ->
(branch_args -> tactic) -> constr option ->
(arg_bindings * arg_bindings) -> constr -> tactic
@@ -148,11 +148,11 @@ val elimination_then :
(arg_bindings * arg_bindings) -> constr -> tactic
val case_then_using :
- case_intro_pattern_expr -> (branch_args -> tactic) ->
+ intro_pattern_expr option -> (branch_args -> tactic) ->
constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
val case_nodep_then_using :
- case_intro_pattern_expr -> (branch_args -> tactic) ->
+ intro_pattern_expr option -> (branch_args -> tactic) ->
constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
val simple_elimination_then :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6444c1756..c069fc1f5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1639,7 +1639,7 @@ let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
(* This was Induction in 6.3 (hybrid form) *)
let induction_from_context_old_style hyp b_ids gl =
let elim_info = find_elim_signature true true None hyp gl in
- let x = induction_from_context true elim_info hyp ([],b_ids) gl in
+ let x = induction_from_context true elim_info hyp (None,b_ids) gl in
(* For translator *) fst (List.hd !b_ids) := true;
x
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b33bc52f0..a12404a9a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -177,7 +177,7 @@ val general_elim_in : identifier -> constr * constr bindings ->
constr * constr bindings -> tactic
val new_induct : constr induction_arg -> constr with_bindings option ->
- case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+ intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
(*s Case analysis tactics. *)
@@ -187,7 +187,7 @@ val simplest_case : constr -> tactic
val simple_destruct : quantified_hypothesis -> tactic
val new_destruct : constr induction_arg -> constr with_bindings option ->
- case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+ intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
(*s Eliminations giving the type instead of the proof. *)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 5704d853b..e5e3a1fa0 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -208,8 +208,8 @@ let pr_with_constr prc = function
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
let pr_with_names = function
- | [] -> mt ()
- | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
+ | None -> mt ()
+ | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
let pr_occs pp = function
[] -> pp
@@ -518,14 +518,14 @@ and pr_atom1 env = function
if List.exists (fun (pp,_) -> !pp) !l then
duplicate true (fun (_,ids) ->
hov 1 (str "induction" ++ spc () ++ pr_arg pr_quantified_hypothesis h ++
- pr_with_names (List.map (fun x -> !x) ids))) !l
+ pr_with_names (Some (IntroOrAndPattern (List.map(fun x -> !x) ids))))) !l
else
hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
| TacNewInduction (h,e,(ids,l)) ->
duplicate false (fun (pp,ids') ->
hov 1 (str "induction" ++ spc () ++
pr_induction_arg (pr_constr env) h ++
- pr_with_names (if !pp then List.map (fun x -> !x) ids' else ids) ++
+ pr_with_names (if !pp then Some (IntroOrAndPattern (List.map (fun x -> !x) ids')) else ids) ++
pr_opt (pr_eliminator env) e)) !l
| TacSimpleDestruct h ->
hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
@@ -533,7 +533,7 @@ and pr_atom1 env = function
duplicate false (fun (pp,ids') ->
hov 1 (str "destruct" ++ spc () ++
pr_induction_arg (pr_constr env) h ++
- pr_with_names (if !pp then List.map (fun x -> !x) ids' else ids)
+ pr_with_names (if !pp then Some (IntroOrAndPattern (List.map (fun x -> !x) ids')) else ids)
++ pr_opt (pr_eliminator env) e)) !l
| TacDoubleInduction (h1,h2) ->
hov 1
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:04:17 +0000