diff options
-rw-r--r-- | contrib/interface/xlate.ml | 21 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
-rw-r--r-- | parsing/g_tacticnew.ml4 | 4 | ||||
-rw-r--r-- | parsing/pptactic.ml | 4 | ||||
-rw-r--r-- | parsing/q_coqast.ml4 | 4 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 8 | ||||
-rw-r--r-- | tactics/hiddentac.mli | 4 | ||||
-rw-r--r-- | tactics/inv.ml | 12 | ||||
-rw-r--r-- | tactics/inv.mli | 10 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 16 | ||||
-rw-r--r-- | tactics/tacticals.ml | 14 | ||||
-rw-r--r-- | tactics/tacticals.mli | 8 | ||||
-rw-r--r-- | tactics/tactics.ml | 2 | ||||
-rw-r--r-- | tactics/tactics.mli | 4 | ||||
-rw-r--r-- | translate/pptacticnew.ml | 10 |
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 |