aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--doc/refman/RefMan-tac.tex17
-rw-r--r--grammar/q_coqast.ml413
-rw-r--r--intf/tacexpr.mli18
-rw-r--r--parsing/g_tactic.ml453
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--printing/pptactic.ml19
-rw-r--r--tactics/contradiction.ml4
-rw-r--r--tactics/equality.ml45
-rw-r--r--tactics/equality.mli8
-rw-r--r--tactics/extratactics.ml46
-rw-r--r--tactics/inv.ml8
-rw-r--r--tactics/tacintern.ml27
-rw-r--r--tactics/tacinterp.ml54
-rw-r--r--tactics/tacsubst.ml17
-rw-r--r--tactics/tactics.ml203
-rw-r--r--tactics/tactics.mli23
-rw-r--r--theories/Init/Wf.v3
-rw-r--r--toplevel/auto_ind_decl.ml12
22 files changed, 349 insertions, 199 deletions
diff --git a/CHANGES b/CHANGES
index e3aa5d792..00f15a62a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -173,6 +173,8 @@ Tactics
- The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
- New tactic "enough", symmetric to "assert", but with subgoals
swapped, as a more friendly replacement of "cut".
+- In destruct/induction, experimental modifier "!" prefixing the
+ hypothesis name to tell not erasing the hypothesis.
Program
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 28d854eaa..a3953bb96 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1573,6 +1573,14 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
and {\tt in} clauses.
+\item{\tt destruct !{\ident}}
+
+ This is a case when the destructed term is an hypothesis of the
+ context. The ``!'' modifier tells to keep the hypothesis in the
+ context after destruction.
+
+ This applies also to the other form of {\tt destruct} and {\tt edestruct}.
+
\item{\tt case \term}\label{case}\tacindex{case}
The tactic {\tt case} is a more basic tactic to perform case
@@ -1750,6 +1758,15 @@ induction n.
einduction}. It combines the effects of the {\tt with}, {\tt as},
{\tt eqn:}, {\tt using}, and {\tt in} clauses.
+\item{\tt induction !{\ident}}
+
+ This is a case when the term on which to apply induction is an
+ hypothesis of the context. The ``!'' modifier tells to keep the
+ hypothesis in the context after induction.
+
+ This applies also to the other form of {\tt induction} and {\tt
+ einduction}.
+
\item {\tt elim \term}\label{elim}
This is a more basic induction tactic. Again, the type of the
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 2690cf867..4fede761f 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -247,6 +247,9 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
let mlexpr_of_constr_with_binding =
mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
+let mlexpr_of_constr_with_binding_arg =
+ mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding
+
let mlexpr_of_move_location f = function
| Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
| Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
@@ -309,13 +312,13 @@ let rec mlexpr_of_atomic_tactic = function
| Tacexpr.TacExact c ->
<:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
| Tacexpr.TacApply (b,false,cb,None) ->
- <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
+ <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding_arg cb$ None >>
| Tacexpr.TacElim (false,cb,cbo) ->
- let cb = mlexpr_of_constr_with_binding cb in
+ let cb = mlexpr_of_constr_with_binding_arg cb in
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
<:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
| Tacexpr.TacCase (false,cb) ->
- let cb = mlexpr_of_constr_with_binding cb in
+ let cb = mlexpr_of_constr_with_binding_arg cb in
<:expr< Tacexpr.TacCase False $cb$ >>
| Tacexpr.TacFix (ido,n) ->
let ido = mlexpr_of_ident_option ido in
@@ -364,7 +367,9 @@ let rec mlexpr_of_atomic_tactic = function
$mlexpr_of_triple
(mlexpr_of_list
(mlexpr_of_pair
- mlexpr_of_induction_arg
+ (mlexpr_of_pair
+ (mlexpr_of_option mlexpr_of_bool)
+ mlexpr_of_induction_arg)
(mlexpr_of_pair
(mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
(mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4174de123..0c5eed714 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -25,14 +25,18 @@ type evars_flag = bool (* true = pose evars false = fail on evars *)
type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
-type 'a induction_arg =
+type 'a core_induction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Id.t located
| ElimOnAnonHyp of int
+type 'a induction_arg =
+ clear_flag * 'a core_induction_arg
+
type inversion_kind =
| SimpleInversion
| FullInversion
@@ -62,6 +66,8 @@ type ('constr,'id) induction_clause_list =
* 'constr with_bindings option (* using ... *)
* 'id clause_expr option (* in ... *)
+type 'a with_bindings_arg = clear_flag * 'a with_bindings
+
type multi =
| Precisely of int
| UpTo of int
@@ -108,10 +114,10 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacIntrosUntil of quantified_hypothesis
| TacIntroMove of Id.t option * 'nam move_location
| TacExact of 'trm
- | TacApply of advanced_flag * evars_flag * 'trm with_bindings list *
- ('nam * intro_pattern_expr located option) option
- | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option
- | TacCase of evars_flag * 'trm with_bindings
+ | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
+ (clear_flag * 'nam * intro_pattern_expr located option) option
+ | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
+ | TacCase of evars_flag * 'trm with_bindings_arg
| TacFix of Id.t option * int
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
| TacCofix of Id.t option
@@ -157,7 +163,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
(* Equality and inversion *)
| TacRewrite of evars_flag *
- (bool * multi * 'trm with_bindings) list * 'nam clause_expr *
+ (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr *
('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
| TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c02f2d569..3c097db1c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -136,19 +136,19 @@ let induction_arg_of_constr (c,lbind as clbind) = match lbind with
| _ -> ElimOnConstr clbind
let mkTacCase with_evar = function
- | [ElimOnConstr cl,(None,None)],None,None ->
- TacCase (with_evar,cl)
+ | [(clear,ElimOnConstr cl),(None,None)],None,None ->
+ TacCase (with_evar,(clear,cl))
(* Reinterpret numbers as a notation for terms *)
- | [ElimOnAnonHyp n,(None,None)],None,None ->
+ | [(clear,ElimOnAnonHyp n),(None,None)],None,None ->
TacCase (with_evar,
- (CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
- NoBindings))
+ (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+ NoBindings)))
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
- | [ElimOnIdent id,(None,None)],None,None ->
- TacCase (with_evar,(CRef (Ident id,None),NoBindings))
+ | [(clear,ElimOnIdent id),(None,None)],None,None ->
+ TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
| ic ->
- if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
+ if List.exists (function ((_, ElimOnAnonHyp _),_) -> true | _ -> false) (pi1 ic)
then
error "Use of numbers as direct arguments of 'case' is not supported.";
TacInductionDestruct (false,with_evar,ic)
@@ -237,10 +237,15 @@ GEXTEND Gram
[ [ c = constr -> c ] ]
;
induction_arg:
- [ [ n = natural -> ElimOnAnonHyp n
- | c = constr_with_bindings -> induction_arg_of_constr c
+ [ [ n = natural -> (None,ElimOnAnonHyp n)
+ | c = constr_with_bindings -> (None,induction_arg_of_constr c)
+ | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c)
] ]
;
+ constr_with_bindings_arg:
+ [ [ ">"; c = constr_with_bindings -> (Some true,c)
+ | c = constr_with_bindings -> (None,c) ] ]
+ ;
quantified_hypothesis:
[ [ id = ident -> NamedHyp id
| n = natural -> AnonHyp n ] ]
@@ -412,7 +417,7 @@ GEXTEND Gram
| -> [] ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
+ [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
| -> None ] ]
;
orient:
@@ -496,12 +501,12 @@ GEXTEND Gram
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
rewriter :
- [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c)
- | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c)
- | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
- | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings -> (UpTo n,c)
- | n = natural; c = constr_with_bindings -> (Precisely n,c)
- | c = constr_with_bindings -> (Precisely 1, c)
+ [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c))
+ | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
+ | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c))
+ | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
+ | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
+ | c = constr_with_bindings -> (Precisely 1, (None,c))
] ]
;
oriented_rewriter :
@@ -534,17 +539,19 @@ GEXTEND Gram
| IDENT "exact"; c = constr -> TacExact c
- | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+ | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp)
- | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ",";
+ | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp)
- | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ",";
+ | IDENT "simple"; IDENT "apply";
+ cl = LIST1 constr_with_bindings_arg SEP ",";
inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp)
- | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP",";
+ | IDENT "simple"; IDENT "eapply";
+ cl = LIST1 constr_with_bindings_arg SEP",";
inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp)
- | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
+ | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
TacElim (false,cl,el)
- | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator ->
+ | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
TacElim (true,cl,el)
| IDENT "case"; icl = induction_clause_list -> mkTacCase false icl
| IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 4218286b0..f780d1bb5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -721,7 +721,7 @@ let rec consider_match may_intro introduced available expected gls =
try conjunction_arity id gls with
Not_found -> error "Matching hypothesis not found." in
tclTHENLIST
- [Proofview.V82.of_tactic (general_case_analysis false (mkVar id,NoBindings));
+ [Proofview.V82.of_tactic (simplest_case (mkVar id));
intron_then nhyps []
(fun l -> consider_match may_intro introduced
(List.rev_append l rest_ids) expected)] gls)
@@ -1313,7 +1313,7 @@ let end_tac et2 gls =
tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)]
| ET_Case_analysis,EK_nodep ->
tclTHEN
- (Proofview.V82.of_tactic (general_case_analysis false (pi.per_casee,NoBindings)))
+ (Proofview.V82.of_tactic (simplest_case pi.per_casee))
(default_justification (List.map mkVar clauses))
| ET_Induction,EK_nodep ->
tclTHENLIST
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 841796ed7..1981fb837 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -976,7 +976,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let rec_id = pf_nth_hyp_id g 1 in
tclTHENSEQ
[(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
- (* observe_tac "h_case" *) (Proofview.V82.of_tactic (general_case_analysis false (mkVar rec_id,NoBindings)));
+ (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
(Proofview.V82.of_tactic intros_reflexivity)] g
)
]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 808b2604c..953e1f049 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,7 +80,7 @@ let functional_induction with_clean c princl pat =
if princ_infos.Tactics.farg_in_concl
then [c] else []
in
- List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
+ List.map (fun c -> None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
in
let princ' = Some (princ,bindings) in
let princ_vars =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 52d3b4a87..5682c2aa4 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -799,7 +799,7 @@ and intros_with_rewrite_aux : tactic =
Proofview.V82.of_tactic Tauto.tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
- Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
+ Proofview.V82.of_tactic (simplest_case v);
intros_with_rewrite
] g
| LetIn _ ->
@@ -836,7 +836,7 @@ let rec reflexivity_with_destruct_cases g =
match kind_of_term (snd (destApp (pf_concl g))).(2) with
| Case(_,_,v,_) ->
tclTHENSEQ[
- Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings));
+ Proofview.V82.of_tactic (simplest_case v);
Proofview.V82.of_tactic intros;
observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
]
@@ -855,7 +855,7 @@ let rec reflexivity_with_destruct_cases g =
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite] g
+ then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
@@ -1013,7 +1013,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
Proofview.V82.of_tactic (Simple.intro graph_principle_id);
observe_tac "" (tclTHEN_i
- (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))))
+ (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
(fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
]
g
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index dbf83936a..7738f0c53 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -120,9 +120,15 @@ let pr_bindings_no_with prc prlc = function
prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| NoBindings -> mt ()
+let pr_keep keep pp x =
+ (if keep then str "!" else mt()) ++ pp x
+
let pr_with_bindings prc prlc (c,bl) =
prc c ++ hv 0 (pr_bindings prc prlc bl)
+let pr_with_bindings_arg prc prlc (keep,c) =
+ pr_keep keep (pr_with_bindings prc prlc) c
+
let pr_with_constr prc = function
| None -> mt ()
| Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
@@ -575,6 +581,7 @@ let make_pr_tac pr_tac_level
let pr_bindings = pr_bindings pr_lconstr pr_constr in
let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
+let pr_with_bindings_arg = pr_with_bindings_arg pr_lconstr pr_constr in
let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
let pr_alias = pr_alias pr_constr pr_lconstr pr_tac_level pr_pat in
let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
@@ -667,13 +674,13 @@ and pr_atom1 = function
| TacApply (a,ev,cb,inhyp) ->
hov 1 ((if a then mt() else str "simple ") ++
str (with_evars ev "apply") ++ spc () ++
- prlist_with_sep pr_comma pr_with_bindings cb ++
+ prlist_with_sep pr_comma pr_with_bindings_arg cb ++
pr_in_hyp_as pr_ident inhyp)
| TacElim (ev,cb,cbo) ->
- hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
+ hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
pr_opt pr_eliminator cbo)
| TacCase (ev,cb) ->
- hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
+ hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
@@ -722,8 +729,8 @@ and pr_atom1 = function
| TacInductionDestruct (isrec,ev,(l,el,cl)) ->
hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
spc () ++
- prlist_with_sep pr_comma (fun (h,ids) ->
- pr_induction_arg pr_lconstr pr_constr h ++
+ prlist_with_sep pr_comma (fun ((keep,h),ids) ->
+ pr_keep keep (pr_induction_arg pr_lconstr pr_constr) h ++
pr_with_induction_names ids) l ++
pr_opt pr_eliminator el ++
pr_opt_no_spc (pr_clauses None pr_ident) cl)
@@ -800,7 +807,7 @@ and pr_atom1 = function
prlist_with_sep
(fun () -> str ","++spc())
(fun (b,m,c) ->
- pr_orient b ++ pr_multi m ++ pr_with_bindings c)
+ pr_orient b ++ pr_multi m ++ pr_with_bindings_arg c)
l
++ pr_clauses (Some true) pr_ident cl
++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 805ecc3eb..96e8e60bb 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -94,7 +94,9 @@ let contradiction_term (c,lbind as cl) =
let typ = type_of c in
let _, ccl = splay_prod env sigma typ in
if is_empty_type ccl then
- Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
+ Tacticals.New.tclTHEN
+ (elim false None cl None)
+ (Tacticals.New.tclTRY assumption)
else
Proofview.tclORELSE
begin
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a23ae4e82..7343aa532 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -460,6 +460,17 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
(general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
do_hyps
+let apply_special_clear_request clear_flag f =
+ Proofview.Goal.raw_enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ try
+ let sigma,(c,bl) = f env sigma in
+ apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
+ with
+ e when catchable_exception e -> tclIDTAC
+ end
+
type delayed_open_constr_with_bindings =
env -> evar_map -> evar_map * constr with_bindings
@@ -484,7 +495,9 @@ let general_multi_multi_rewrite with_evars l cl tac =
in
let rec loop = function
| [] -> Proofview.tclUNIT ()
- | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
+ | (l2r,m,clear_flag,c)::l ->
+ tclTHENFIRST
+ (tclTHEN (doN l2r c m) (apply_special_clear_request clear_flag c)) (loop l)
in loop l
let rewriteLR = general_rewrite true AllOccurrences true true
@@ -963,7 +976,7 @@ let discrEverywhere with_evars =
*)
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
- | Some c -> onInductionArg (discr with_evars) c
+ | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
let discrConcl = discrClause false onConcl
let discrHyp id = discrClause false (onHyp id)
@@ -1296,13 +1309,15 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
inject_at_positions env sigma l2r u eq_clause posns
(tac (clenv_value eq_clause))
-let postInjEqTac ipats c n =
+let use_clear_hyp_by_default () = false
+
+let postInjEqTac clear_flag ipats c n =
match ipats with
| Some ipats ->
let clear_tac =
- if use_injection_pattern_l2r_order () && isVar c
- then tclTRY (clear [destVar c])
- else tclIDTAC in
+ let dft =
+ use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in
+ tclTRY (apply_clear_request clear_flag dft c) in
let intro_tac =
if use_injection_pattern_l2r_order ()
then intros_pattern_bound n MoveLast ipats
@@ -1310,20 +1325,20 @@ let postInjEqTac ipats c n =
tclTHEN clear_tac intro_tac
| None -> tclIDTAC
-let injEq ipats =
+let injEq clear_flag ipats =
let l2r =
if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
in
- injEqThen (fun c i -> postInjEqTac ipats c i) l2r
+ injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r
-let inj ipats with_evars = onEquality with_evars (injEq ipats)
+let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats)
let injClause ipats with_evars = function
- | None -> onNegatedEquality with_evars (injEq ipats)
+ | None -> onNegatedEquality with_evars (injEq None ipats)
| Some c -> onInductionArg (inj ipats with_evars) c
let injConcl = injClause None false None
-let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
+let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
@@ -1341,10 +1356,12 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
end
let dEqThen with_evars ntac = function
- | None -> onNegatedEquality with_evars (decompEqThen ntac)
- | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
+ | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
+ | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
-let dEq with_evars = dEqThen with_evars (fun c x -> Proofview.tclUNIT ())
+let dEq with_evars =
+ dEqThen with_evars (fun clear_flag c x ->
+ (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decompe_eq tac data cl =
Proofview.Goal.raw_enter begin fun gl ->
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 82e30b940..2993c8d3a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -64,7 +64,7 @@ type delayed_open_constr_with_bindings =
env -> evar_map -> evar_map * constr with_bindings
val general_multi_multi_rewrite :
- evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list ->
+ evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic
@@ -78,14 +78,14 @@ val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
constr with_bindings induction_arg option -> unit Proofview.tactic
val inj : intro_pattern_expr Loc.located list option -> evars_flag ->
- constr with_bindings -> unit Proofview.tactic
+ clear_flag -> constr with_bindings -> unit Proofview.tactic
val injClause : intro_pattern_expr Loc.located list option -> evars_flag ->
constr with_bindings induction_arg option -> unit Proofview.tactic
-val injHyp : Id.t -> unit Proofview.tactic
+val injHyp : clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : unit Proofview.tactic
val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic
+val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8cf1e531d..a7d95c5e8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -65,8 +65,8 @@ TACTIC EXTEND replace_term
END
let induction_arg_of_quantified_hyp = function
- | AnonHyp n -> ElimOnAnonHyp n
- | NamedHyp id -> ElimOnIdent (Loc.ghost,id)
+ | AnonHyp n -> None,ElimOnAnonHyp n
+ | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id)
(* Versions *_main must come first!! so that "1" is interpreted as a
ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
@@ -74,7 +74,7 @@ let induction_arg_of_quantified_hyp = function
let elimOnConstrWithHoles tac with_evars c =
Tacticals.New.tclWITHHOLES with_evars (tac with_evars)
- c.sigma (Some (ElimOnConstr c.it))
+ c.sigma (Some (None,ElimOnConstr c.it))
TACTIC EXTEND simplify_eq_main
| [ "simplify_eq" constr_with_bindings(c) ] ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ee875ce27..36affb541 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -308,9 +308,11 @@ let projectAndApply thin id eqname names depids =
| _ -> tac id
end
in
- let deq_trailer id _ neqns =
+ let deq_trailer id clear_flag _ neqns =
tclTHENLIST
- [(if not (List.is_empty names) then clear [id] else tclIDTAC);
+ [apply_clear_request clear_flag
+ (not (List.is_empty names) || use_clear_hyp_by_default ())
+ (mkVar id);
(tclMAP_i neqns (fun idopt ->
tclTRY (tclTHEN
(intro_move idopt MoveLast)
@@ -325,7 +327,7 @@ let projectAndApply thin id eqname names depids =
(* and apply a trailer which again try to substitute *)
(fun id ->
dEqThen false (deq_trailer id)
- (Some (ElimOnConstr (mkVar id,NoBindings))))
+ (Some (None,ElimOnConstr (mkVar id,NoBindings))))
id
let nLastDecls i tac =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index e2f87062e..80711cf81 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -270,18 +270,21 @@ let intern_bindings ist = function
let intern_constr_with_bindings ist (c,bl) =
(intern_constr ist c, intern_bindings ist bl)
+let intern_constr_with_bindings_arg ist (clear,c) =
+ (clear,intern_constr_with_bindings ist c)
+
(* TODO: catch ltac vars *)
let intern_induction_arg ist = function
- | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
- | ElimOnAnonHyp n as x -> x
- | ElimOnIdent (loc,id) ->
+ | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
+ | clear,ElimOnAnonHyp n as x -> x
+ | clear,ElimOnIdent (loc,id) ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
match intern_constr ist (CRef (Ident (dloc,id), None)) with
- | GVar (loc,id),_ -> ElimOnIdent (loc,id)
- | c -> ElimOnConstr (c,NoBindings)
+ | GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
+ | c -> clear,ElimOnConstr (c,NoBindings)
else
- ElimOnIdent (loc,id)
+ clear,ElimOnIdent (loc,id)
let short_name = function
| AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
@@ -371,8 +374,8 @@ let intern_red_expr ist = function
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
-let intern_in_hyp_as ist lf (id,ipat) =
- (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
+let intern_in_hyp_as ist lf (clear,id,ipat) =
+ (clear,intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
let intern_hyp_list ist = List.map (intern_hyp ist)
@@ -459,12 +462,12 @@ let rec intern_atomic lf ist x =
intern_move_location ist hto)
| TacExact c -> TacExact (intern_constr ist c)
| TacApply (a,ev,cb,inhyp) ->
- TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
+ TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
Option.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
- TacElim (ev,intern_constr_with_bindings ist cb,
+ TacElim (ev,intern_constr_with_bindings_arg ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
- | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
+ | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb)
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
| TacMutualFix (id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
@@ -555,7 +558,7 @@ let rec intern_atomic lf ist x =
| TacRewrite (ev,l,cl,by) ->
TacRewrite
(ev,
- List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+ List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings_arg ist c)) l,
clause_app (intern_hyp_location ist) cl,
Option.map (intern_pure_tactic ist) by)
| TacInversion (inv,hyp) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b52a3e7e9..0432b08ec 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -768,8 +768,8 @@ and interp_intro_pattern_list_as_list ist env = function
List.map (interp_intro_pattern ist env) l)
| l -> List.map (interp_intro_pattern ist env) l
-let interp_in_hyp_as ist env (id,ipat) =
- (interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
+let interp_in_hyp_as ist env (clear,id,ipat) =
+ (clear,interp_hyp ist env id,Option.map (interp_intro_pattern ist env) ipat)
let interp_quantified_hypothesis ist = function
| AnonHyp n -> AnonHyp n
@@ -812,11 +812,19 @@ let interp_constr_with_bindings ist env sigma (c,bl) =
let sigma, c = interp_open_constr ist env sigma c in
sigma, (c,bl)
+let interp_constr_with_bindings_arg ist env sigma (keep,c) =
+ let sigma, c = interp_constr_with_bindings ist env sigma c in
+ sigma, (keep,c)
+
let interp_open_constr_with_bindings ist env sigma (c,bl) =
let sigma, bl = interp_bindings ist env sigma bl in
let sigma, c = interp_open_constr ist env sigma c in
sigma, (c, bl)
+let interp_open_constr_with_bindings_arg ist env sigma (keep,c) =
+ let sigma, c = interp_open_constr_with_bindings ist env sigma c in
+ sigma,(keep,c)
+
let loc_of_bindings = function
| NoBindings -> Loc.ghost
| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
@@ -829,22 +837,26 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
sigma, (loc,cb)
+let interp_open_constr_with_bindings_arg_loc ist env sigma (keep,c) =
+ let sigma, c = interp_open_constr_with_bindings_loc ist env sigma c in
+ sigma,(keep,c)
+
let interp_induction_arg ist gl arg =
let env = pf_env gl and sigma = project gl in
match arg with
- | ElimOnConstr c ->
- ElimOnConstr (interp_constr_with_bindings ist env sigma c)
- | ElimOnAnonHyp n as x -> x
- | ElimOnIdent (loc,id) ->
+ | keep,ElimOnConstr c ->
+ keep,ElimOnConstr (interp_constr_with_bindings ist env sigma c)
+ | keep,ElimOnAnonHyp n as x -> x
+ | keep,ElimOnIdent (loc,id) ->
let error () = user_err_loc (loc, "",
strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
let try_cast_id id' =
if Tactics.is_quantified_hypothesis id' gl
- then ElimOnIdent (loc,id')
+ then keep,ElimOnIdent (loc,id')
else
- (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
+ (try keep,ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
with Not_found ->
user_err_loc (loc,"",
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
@@ -862,18 +874,18 @@ let interp_induction_arg ist gl arg =
let id = out_gen (topwit wit_var) v in
try_cast_id id
else if has_type v (topwit wit_int) then
- ElimOnAnonHyp (out_gen (topwit wit_int) v)
+ keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
else match Value.to_constr v with
| None -> error ()
- | Some c -> ElimOnConstr (sigma,(c,NoBindings))
+ | Some c -> keep,ElimOnConstr (sigma,(c,NoBindings))
with Not_found ->
(* We were in non strict (interactive) mode *)
if Tactics.is_quantified_hypothesis id gl then
- ElimOnIdent (loc,id)
+ keep,ElimOnIdent (loc,id)
else
let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
let (sigma,c) = interp_constr ist env sigma c in
- ElimOnConstr (sigma,(c,NoBindings))
+ keep,ElimOnConstr (sigma,(c,NoBindings))
(* Associates variables with values and gives the remaining variables and
values *)
@@ -1544,7 +1556,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, l =
- List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+ List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb
in
let tac = match cl with
| None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
@@ -1552,25 +1564,25 @@ and interp_atomic ist tac : unit Proofview.tactic =
(fun l ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let (id,cl) = interp_in_hyp_as ist env cl in
- Tactics.apply_in a ev id l cl
+ let (clear,id,cl) = interp_in_hyp_as ist env cl in
+ Tactics.apply_in a ev clear id l cl
end) in
Tacticals.New.tclWITHHOLES ev tac sigma l
end
- | TacElim (ev,cb,cbo) ->
+ | TacElim (ev,(keep,cb),cbo) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
- Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
+ Tacticals.New.tclWITHHOLES ev (Tactics.elim ev keep cb) sigma cbo
end
- | TacCase (ev,cb) ->
+ | TacCase (ev,(keep,cb)) ->
Proofview.Goal.raw_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
- Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
+ Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev keep) sigma cb
end
| TacFix (idopt,n) ->
Proofview.Goal.raw_enter begin fun gl ->
@@ -1824,9 +1836,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
Proofview.Goal.raw_enter begin fun gl ->
- let l = List.map (fun (b,m,c) ->
+ let l = List.map (fun (b,m,(keep,c)) ->
let f env sigma = interp_open_constr_with_bindings ist env sigma c in
- (b,m,f)) l in
+ (b,m,keep,f)) l in
let env = Proofview.Goal.env gl in
let cl = interp_clause ist env cl in
Equality.general_multi_multi_rewrite ev l cl
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 428061463..0ff4fe9b8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -44,10 +44,13 @@ let subst_bindings subst = function
let subst_glob_with_bindings subst (c,bl) =
(subst_glob_constr subst c, subst_bindings subst bl)
+let subst_glob_with_bindings_arg subst (clear,c) =
+ (clear,subst_glob_with_bindings subst c)
+
let subst_induction_arg subst = function
- | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c)
- | ElimOnAnonHyp n as x -> x
- | ElimOnIdent id as x -> x
+ | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
+ | clear,ElimOnAnonHyp n as x -> x
+ | clear,ElimOnIdent id as x -> x
let subst_and_short_name f (c,n) =
(* assert (n=None); *)(* since tacdef are strictly globalized *)
@@ -135,11 +138,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
| TacExact c -> TacExact (subst_glob_constr subst c)
| TacApply (a,ev,cb,cl) ->
- TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
+ TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
| TacElim (ev,cb,cbo) ->
- TacElim (ev,subst_glob_with_bindings subst cb,
+ TacElim (ev,subst_glob_with_bindings_arg subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
- | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
+ | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb)
| TacFix (idopt,n) as x -> x
| TacMutualFix (id,n,l) ->
TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
@@ -194,7 +197,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacRewrite (ev,l,cl,by) ->
TacRewrite (ev,
List.map (fun (b,m,c) ->
- b,m,subst_glob_with_bindings subst c) l,
+ b,m,subst_glob_with_bindings_arg subst c) l,
cl,Option.map (subst_tactic subst) by)
| TacInversion (DepInversion (k,c,l),hyp) ->
TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb6894fef..2de4e26f3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -99,6 +99,19 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> apply_solve_class_goals:=a);
}
+let clear_hyp_by_default = ref false
+
+let use_clear_hyp_by_default () = !clear_hyp_by_default
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "default clearing of hypotheses after use";
+ optkey = ["Default";"Clearing";"Used";"Hypotheses"];
+ optread = (fun () -> !clear_hyp_by_default) ;
+ optwrite = (fun b -> clear_hyp_by_default := b) }
+
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -159,6 +172,16 @@ let thin l gl =
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
+let apply_clear_request clear_flag dft c =
+ let check_isvar c =
+ if not (isVar c) then
+ error "keep/clear modifiers apply only to hypothesis names." in
+ let clear = match clear_flag with
+ | None -> dft && isVar c
+ | Some clear -> check_isvar c; clear in
+ if clear then Proofview.V82.tactic (thin [destVar c])
+ else Tacticals.New.tclIDTAC
+
let internal_cut_gen b d t gl =
try internal_cut b d t gl
with Evarutil.ClearDependencyError (id,err) ->
@@ -167,8 +190,8 @@ let internal_cut_gen b d t gl =
let internal_cut = internal_cut_gen false
let internal_cut_replace = internal_cut_gen true
-let internal_cut_rev_gen b d t gl =
- try internal_cut_rev b d t gl
+let internal_cut_rev_gen b id t gl =
+ try internal_cut_rev b id t gl
with Evarutil.ClearDependencyError (id,err) ->
error_clear_dependency (pf_env gl) id err
@@ -678,31 +701,36 @@ let rec intros_move = function
or a term with bindings *)
let onOpenInductionArg tac = function
- | ElimOnConstr cbl ->
- tac cbl
- | ElimOnAnonHyp n ->
+ | clear_flag,ElimOnConstr cbl ->
+ tac clear_flag cbl
+ | clear_flag,ElimOnAnonHyp n ->
Tacticals.New.tclTHEN
(intros_until_n n)
- (Tacticals.New.onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings))))
- | ElimOnIdent (_,id) ->
+ (Tacticals.New.onLastHyp
+ (fun c -> tac clear_flag (Evd.empty,(c,NoBindings))))
+ | clear_flag,ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
- (tac (Evd.empty,(mkVar id,NoBindings)))
+ (tac clear_flag (Evd.empty,(mkVar id,NoBindings)))
let onInductionArg tac = function
- | ElimOnConstr cbl ->
- tac cbl
- | ElimOnAnonHyp n ->
- Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac (c,NoBindings)))
- | ElimOnIdent (_,id) ->
+ | clear_flag,ElimOnConstr cbl ->
+ tac clear_flag cbl
+ | clear_flag,ElimOnAnonHyp n ->
+ Tacticals.New.tclTHEN
+ (intros_until_n n)
+ (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
+ | clear_flag,ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
- Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings))
+ Tacticals.New.tclTHEN
+ (try_intros_until_id_check id)
+ (tac clear_flag (mkVar id,NoBindings))
let map_induction_arg f = function
- | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl)
- | ElimOnAnonHyp n -> ElimOnAnonHyp n
- | ElimOnIdent id -> ElimOnIdent id
+ | clear_flag,ElimOnConstr (sigma,(c,bl)) -> clear_flag,ElimOnConstr (f (sigma,c),bl)
+ | clear_flag,ElimOnAnonHyp n as x -> x
+ | clear_flag,ElimOnIdent id as x -> x
(**************************)
(* Cut tactics *)
@@ -782,13 +810,19 @@ let check_unresolved_evars_of_metas clenv =
| _ -> ())
(meta_list clenv.evd)
+let clear_of_flag flag =
+ match flag with
+ | None -> true (* default for apply in *)
+ | Some b -> b
+
(* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last
ones (resp [n] first ones if [sidecond_first] is [true]) being the
[Ti] and the first one (resp last one) being [G] whose hypothesis
[id] is replaced by P using the proof given by [tac] *)
-let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl =
+let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) clear_flag id clenv gl =
+ let with_clear = clear_of_flag clear_flag in
let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
let clenv =
if with_classes then
@@ -800,10 +834,15 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
if not with_evars && occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
+ let id' = if with_clear then id else fresh_id [] id gl in
+ let exact_tac = refine_no_check new_hyp_prf in
tclTHEN
(tclEVARS clenv.evd)
- ((if sidecond_first then assert_replacing else cut_replacing)
- id new_hyp_typ (refine_no_check new_hyp_prf)) gl
+ (if sidecond_first then
+ tclTHENFIRST (internal_cut_gen with_clear id' new_hyp_typ) exact_tac
+ else
+ tclTHENLAST (internal_cut_rev_gen with_clear id' new_hyp_typ) exact_tac)
+ gl
(********************************************)
(* Elimination tactics *)
@@ -900,16 +939,20 @@ let general_elim_clause_gen elimtac indclause elim gl =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl
-let general_elim with_evars (c, lbindc) elim gl =
+let general_elim with_evars clear_flag (c, lbindc) elim gl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
let elimtac = elimination_clause_scheme with_evars in
let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in
- general_elim_clause_gen elimtac indclause elim gl
+ tclTHEN
+ (general_elim_clause_gen elimtac indclause elim)
+ (Proofview.V82.of_tactic
+ (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
+ gl
(* Case analysis tactics *)
-let general_case_analysis_in_context with_evars (c,lbindc) gl =
+let general_case_analysis_in_context with_evars clear_flag (c,lbindc) gl =
let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
let sort = elimination_sort_of_goal gl in
let sigma, elim =
@@ -918,19 +961,21 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
else
pf_apply build_case_analysis_scheme_default gl mind sort in
tclTHEN (tclEVARS sigma)
- (general_elim with_evars (c,lbindc)
+ (general_elim with_evars clear_flag (c,lbindc)
{elimindex = None; elimbody = (elim,NoBindings);
elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl
-let general_case_analysis with_evars (c,lbindc as cx) =
+let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
match kind_of_term c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
- (Proofview.V82.tactic (general_case_analysis_in_context with_evars cx))
+ (Proofview.V82.tactic
+ (general_case_analysis_in_context with_evars clear_flag cx))
| _ ->
- Proofview.V82.tactic (general_case_analysis_in_context with_evars cx)
+ Proofview.V82.tactic
+ (general_case_analysis_in_context with_evars clear_flag cx)
-let simplest_case c = general_case_analysis false (c,NoBindings)
+let simplest_case c = general_case_analysis false None (c,NoBindings)
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
@@ -951,39 +996,39 @@ let find_eliminator c gl =
evd, {elimindex = None; elimbody = (c,NoBindings);
elimrename = Some (true, constructors_nrealdecls ind)}
-let default_elim with_evars (c,_ as cx) =
+let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
(Proofview.Goal.raw_enter begin fun gl ->
let evd, elim = find_eliminator c gl in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
- (Proofview.V82.tactic (general_elim with_evars cx elim))
+ (Proofview.V82.tactic (general_elim with_evars clear_flag cx elim))
end)
begin function
| IsRecord ->
(* For records, induction principles aren't there by default
anymore. Instead, we do a case analysis instead. *)
- general_case_analysis with_evars cx
+ general_case_analysis with_evars clear_flag cx
| e -> Proofview.tclZERO e
end
-let elim_in_context with_evars c = function
+let elim_in_context with_evars clear_flag c = function
| Some elim ->
Proofview.V82.tactic
- (general_elim with_evars c {elimindex = Some (-1); elimbody = elim;
+ (general_elim with_evars clear_flag c {elimindex = Some (-1); elimbody = elim;
elimrename = None})
- | None -> default_elim with_evars c
+ | None -> default_elim with_evars clear_flag c
-let elim with_evars (c,lbindc as cx) elim =
+let elim with_evars clear_flag (c,lbindc as cx) elim =
match kind_of_term c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
- (elim_in_context with_evars cx elim)
+ (elim_in_context with_evars clear_flag cx elim)
| _ ->
- elim_in_context with_evars cx elim
+ elim_in_context with_evars clear_flag cx elim
(* The simplest elimination tactic, with no substitutions at all. *)
-let simplest_elim c = default_elim false (c,NoBindings)
+let simplest_elim c = default_elim false None (c,NoBindings)
(* Elimination in hypothesis *)
(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
@@ -1019,7 +1064,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (
if eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
- clenv_refine_in with_evars id elimclause'' gl
+ clenv_refine_in with_evars None id elimclause'' gl
let general_elim_clause with_evars flags id c e =
let elim = match id with
@@ -1117,7 +1162,7 @@ let solve_remaining_apply_goals gl =
with Not_found -> tclIDTAC gl
else tclIDTAC gl
-let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
+let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) gl0 =
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
@@ -1153,21 +1198,26 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
Loc.raise loc exn
in try_red_apply thm_ty0
in
- tclTHEN (try_main_apply with_destruct c) solve_remaining_apply_goals gl0
+ tclTHENLIST [
+ try_main_apply with_destruct c;
+ solve_remaining_apply_goals;
+ Proofview.V82.of_tactic
+ (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
+ ] gl0
let rec apply_with_bindings_gen b e = function
| [] -> tclIDTAC
- | [cb] -> general_apply b b e cb
- | cb::cbl ->
- tclTHENLAST (general_apply b b e cb) (apply_with_bindings_gen b e cbl)
+ | [k,cb] -> general_apply b b e k cb
+ | (k,cb)::cbl ->
+ tclTHENLAST (general_apply b b e k cb) (apply_with_bindings_gen b e cbl)
-let apply_with_bindings cb = apply_with_bindings_gen false false [dloc,cb]
+let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
-let eapply_with_bindings cb = apply_with_bindings_gen false true [dloc,cb]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
-let apply c = apply_with_bindings_gen false false [dloc,(c,NoBindings)]
+let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))]
-let eapply c = apply_with_bindings_gen false true [dloc,(c,NoBindings)]
+let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))]
let apply_list = function
| c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1212,15 +1262,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
in
aux (pf_apply make_clenv_binding gl (d,thm) lbind)
-let apply_in_once sidecond_first with_delta with_destruct with_evars id
- (loc,(d,lbind)) gl0 =
+let apply_in_once sidecond_first with_delta with_destruct with_evars hyp_clear_flag
+ id (clear_flag,(loc,(d,lbind))) gl0 =
let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
let t' = pf_get_hyp_typ gl0 id in
let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
let rec aux with_destruct c gl =
try
let clause = apply_in_once_main flags innerclause (c,lbind) gl in
- clenv_refine_in ~sidecond_first with_evars id clause gl
+ tclTHEN
+ (clenv_refine_in ~sidecond_first with_evars hyp_clear_flag id clause)
+ (Proofview.V82.of_tactic
+ (apply_clear_request clear_flag false c))
+ gl
with e when with_destruct ->
let e = Errors.push e in
descend_in_conjunctions aux (fun _ -> raise e) c gl
@@ -1435,7 +1489,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
(Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (fst mind, i) in
let cons = mkConstructU cons in
- let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+ let apply_tac = Proofview.V82.tactic (general_apply true false with_evars None (dloc,(cons,lbind))) in
(Tacticals.New.tclTHENLIST
[Proofview.V82.tclEVARS sigma; Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
end
@@ -1770,23 +1824,23 @@ let tclMAPFIRST tacfun l =
List.fold_right (fun x -> Tacticals.New.tclTHENFIRST (tacfun x)) l (Proofview.tclUNIT())
let general_apply_in sidecond_first with_delta with_destruct with_evars
- id lemmas ipat =
+ with_clear id lemmas ipat =
if sidecond_first then
(* Skip the side conditions of the applied lemma *)
Tacticals.New.tclTHENLAST
(tclMAPLAST
- (apply_in_once sidecond_first with_delta with_destruct with_evars id)
+ (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
lemmas)
(as_tac id ipat)
else
Tacticals.New.tclTHENFIRST
(tclMAPFIRST
- (apply_in_once sidecond_first with_delta with_destruct with_evars id)
+ (apply_in_once sidecond_first with_delta with_destruct with_evars with_clear id)
lemmas)
(as_tac id ipat)
-let apply_in simple with_evars id lemmas ipat =
- general_apply_in false simple simple with_evars id lemmas ipat
+let apply_in simple with_evars clear_flag id lemmas ipat =
+ general_apply_in false simple simple with_evars clear_flag id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
@@ -3283,7 +3337,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
let elimc = mkCast (elimc, DEFAULTcast, elimt) in
elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl
-let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
+let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
inhyps =
Proofview.Goal.enter begin fun gl ->
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
@@ -3295,18 +3349,19 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
induction_tac with_evars elim (hyp0,lbind) typ0;
tclTRY (unfold_body hyp0);
- thin [hyp0]
+ Proofview.V82.of_tactic
+ (apply_clear_request clear_flag true (mkVar hyp0))
]) in
apply_induction_in_context
(Some (hyp0,inhyps)) elim indvars names induct_tac
end
-let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
+let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names (hyp0,lbind) inhyps =
Proofview.Goal.enter begin fun gl ->
let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
Tacticals.New.tclTHENLIST
[Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
- (induction_from_context isrec with_evars elim_info
+ (induction_from_context clear_flag isrec with_evars elim_info
(hyp0,lbind) names inhyps)]
end
@@ -3358,7 +3413,7 @@ let clear_unselected_context id inhyps cls gl =
thin ids gl
| None -> tclIDTAC gl
-let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
+let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
let inhyps = match cls with
| Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
| _ -> [] in
@@ -3369,7 +3424,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
Tacticals.New.tclTHEN
(Proofview.V82.tactic (clear_unselected_context id inhyps cls))
(induction_with_atomization_of_ind_arg
- isrec with_evars elim names (id,lbind) inhyps)
+ clear_flag isrec with_evars elim names (id,lbind) inhyps)
| _ ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -3385,7 +3440,8 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
(letin_tac_gen with_eq
(AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None)
(induction_with_atomization_of_ind_arg
- isrec with_evars elim names (id,lbind) inhyps)
+ (Some true)
+ isrec with_evars elim names (id,lbind) inhyps)
end
end
@@ -3447,7 +3503,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
if Int.equal (List.length lc) 1 && not ifi then
(* standard induction *)
onOpenInductionArg
- (fun c -> induction_gen isrec with_evars elim names c cls)
+ (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim names c cls)
(List.hd lc)
else begin
(* functional induction *)
@@ -3467,7 +3523,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
(* Hook to recover standard induction on non-standard induction schemes *)
(* will be removable when is_functional_induction will be more clever *)
onInductionArg
- (fun (c,lbind) ->
+ (fun _clear_flag (c,lbind) ->
if lbind != NoBindings then
error "'with' clause not supported here.";
induction_gen_l isrec with_evars elim names [c]) (List.hd lc)
@@ -3475,7 +3531,7 @@ let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
let newlc =
List.map (fun x ->
match x with (* FIXME: should we deal with ElimOnIdent? *)
- | ElimOnConstr (x,NoBindings) -> x
+ | _clear_flag,ElimOnConstr (x,NoBindings) -> x
| _ -> error "Don't know where to find some argument.")
lc in
induction_gen_l isrec with_evars elim names newlc
@@ -3910,10 +3966,15 @@ module Simple = struct
generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
cl)
- let apply c = apply_with_bindings_gen false false [Loc.ghost,(c,NoBindings)]
- let eapply c = apply_with_bindings_gen false true [Loc.ghost,(c,NoBindings)]
- let elim c = elim false (c,NoBindings) None
- let case c = general_case_analysis false (c,NoBindings)
+ let apply c =
+ apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
+ let eapply c =
+ apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))]
+ let elim c = elim false None (c,NoBindings) None
+ let case c = general_case_analysis false None (c,NoBindings)
+
+ let apply_in id c =
+ apply_in false false None id [None,(Loc.ghost, (c, NoBindings))] None
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c2403d97a..f58e218be 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -93,9 +93,13 @@ val try_intros_until :
or a term with bindings *)
val onInductionArg :
- (constr with_bindings -> unit Proofview.tactic) ->
+ (clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
constr with_bindings induction_arg -> unit Proofview.tactic
+(** Tell if a used hypothesis should be cleared by default or not *)
+
+val use_clear_hyp_by_default : unit -> bool
+
(** {6 Introduction tactics with eliminations. } *)
val intro_pattern : Id.t move_location -> intro_pattern_expr -> unit Proofview.tactic
@@ -157,6 +161,7 @@ val unfold_constr : global_reference -> tactic
val clear : Id.t list -> tactic
val clear_body : Id.t list -> tactic
val keep : Id.t list -> tactic
+val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
val specialize : constr with_bindings -> tactic
@@ -174,7 +179,7 @@ val apply : constr -> tactic
val eapply : constr -> tactic
val apply_with_bindings_gen :
- advanced_flag -> evars_flag -> constr with_bindings located list -> tactic
+ advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> tactic
val apply_with_bindings : constr with_bindings -> tactic
val eapply_with_bindings : constr with_bindings -> tactic
@@ -182,8 +187,8 @@ val eapply_with_bindings : constr with_bindings -> tactic
val cut_and_apply : constr -> unit Proofview.tactic
val apply_in :
- advanced_flag -> evars_flag -> Id.t ->
- constr with_bindings located list ->
+ advanced_flag -> evars_flag -> clear_flag -> Id.t ->
+ (clear_flag * constr with_bindings located) list ->
intro_pattern_expr located option -> unit Proofview.tactic
(** {6 Elimination tactics. } *)
@@ -245,16 +250,17 @@ type eliminator = {
elimbody : constr with_bindings
}
-val general_elim : evars_flag ->
+val general_elim : evars_flag -> clear_flag ->
constr with_bindings -> eliminator -> tactic
val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
clausenv -> eliminator -> unit Proofview.tactic
-val default_elim : evars_flag -> constr with_bindings -> unit Proofview.tactic
+val default_elim : evars_flag -> clear_flag -> constr with_bindings ->
+ unit Proofview.tactic
val simplest_elim : constr -> unit Proofview.tactic
val elim :
- evars_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
+ evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic
val simple_induct : quantified_hypothesis -> unit Proofview.tactic
@@ -266,7 +272,7 @@ val induction : evars_flag ->
(** {6 Case analysis tactics. } *)
-val general_case_analysis : evars_flag -> constr with_bindings -> unit Proofview.tactic
+val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic
val simplest_case : constr -> unit Proofview.tactic
val simple_destruct : quantified_hypothesis -> unit Proofview.tactic
@@ -384,6 +390,7 @@ module Simple : sig
val eapply : constr -> tactic
val elim : constr -> unit Proofview.tactic
val case : constr -> unit Proofview.tactic
+ val apply_in : identifier -> constr -> unit Proofview.tactic
end
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 9b4c62f87..1e8fad98e 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -169,5 +169,4 @@ Section Acc_generator.
end.
-End Acc_generator.
- \ No newline at end of file
+End Acc_generator.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0fbf0654f..15b370b06 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -79,12 +79,12 @@ let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
let induct_on c =
induction false
- [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+ [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None (None,None) None
let destruct_on_using c id =
destruct false
- [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+ [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None
(None,Some (dl,IntroOrAndPattern [
[dl,IntroAnonymous];
@@ -93,7 +93,7 @@ let destruct_on_using c id =
let destruct_on c =
destruct false
- [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
+ [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None (None,None) None
(* reconstruct the inductive with the correct deBruijn indexes *)
@@ -589,10 +589,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
- apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None;
+ Simple.apply_in freshz (andb_prop());
Proofview.Goal.enter begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
- (destruct false [Tacexpr.ElimOnConstr
+ (destruct false [None,Tacexpr.ElimOnConstr
(Evd.empty,((mkVar freshz,NoBindings)))]
None
(None, Some (dl,IntroOrAndPattern [[
@@ -723,7 +723,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTRY (
Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
);
- Equality.inj None false (mkVar freshz,NoBindings);
+ Equality.inj None false None (mkVar freshz,NoBindings);
intros; (Proofview.V82.tactic simpl_in_concl);
Auto.default_auto;
Tacticals.New.tclREPEAT (
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 21:43:14 +0000