aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/firstorder/rules.ml2
-rw-r--r--contrib/funind/functional_principles_proofs.ml2
-rw-r--r--contrib/funind/recdef.ml2
-rw-r--r--contrib/interface/xlate.ml1
-rw-r--r--contrib/setoid_ring/newring.ml41
-rw-r--r--parsing/g_tactic.ml41
-rw-r--r--parsing/pptactic.ml1
-rw-r--r--parsing/q_coqast.ml412
-rw-r--r--pretyping/termops.ml17
-rw-r--r--pretyping/termops.mli9
-rw-r--r--proofs/tacexpr.ml7
-rw-r--r--tactics/dhyp.ml1
-rw-r--r--tactics/evar_tactics.mli1
-rw-r--r--tactics/extraargs.ml43
-rw-r--r--tactics/extraargs.mli1
-rw-r--r--tactics/extratactics.ml410
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/tactics.ml151
-rw-r--r--tactics/tactics.mli3
-rw-r--r--theories/NArith/Ndigits.v6
-rw-r--r--toplevel/auto_ind_decl.ml4
21 files changed, 168 insertions, 69 deletions
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index 813e951cf..6c00e4eac 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -213,4 +213,4 @@ let normalize_evaluables=
None->unfold_in_concl (Lazy.force defined_connectives)
| Some ((_,id),_)->
unfold_in_hyp (Lazy.force defined_connectives)
- ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly))
+ ((Rawterm.all_occurrences_expr,id),InHypTypeOnly))
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 971dada68..6241eb1de 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1347,7 +1347,7 @@ let build_clause eqs =
{
Tacexpr.onhyps =
Some (List.map
- (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
+ (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
eqs
);
Tacexpr.concl_occs = Rawterm.no_occurrences_expr
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 8161e890d..528c276c0 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -1160,7 +1160,7 @@ let rec introduce_all_values_eq cont_tac functional termine
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
(global_of_constr functional))]
- ((all_occurrences_expr, heq2), Tacexpr.InHyp);
+ ((all_occurrences_expr, heq2), InHyp);
tclTHENS
(fun gls ->
let t_eq = compute_renamed_type gls (mkVar heq2) in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7b654b74b..26b9be870 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -7,6 +7,7 @@ open Names;;
open Ascent;;
open Genarg;;
open Rawterm;;
+open Termops;;
open Tacexpr;;
open Vernacexpr;;
open Decl_kinds;;
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c3bc458e2..fc66b1c97 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -19,6 +19,7 @@ open Environ
open Libnames
open Tactics
open Rawterm
+open Termops
open Tacticals
open Tacexpr
open Pcoq
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ec84c6ed8..2276800d5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -18,6 +18,7 @@ open Rawterm
open Genarg
open Topconstr
open Libnames
+open Termops
let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index b37cb9fce..77eec5e60 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -21,6 +21,7 @@ open Pattern
open Ppextend
open Ppconstr
open Printer
+open Termops
let pr_global x = Nametab.pr_global_env Idset.empty x
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 1a5e7fb72..9c1a10b0e 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -103,12 +103,12 @@ let mlexpr_of_occs =
let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
let mlexpr_of_hyp_location = function
- | occs, Tacexpr.InHyp ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >>
- | occs, Tacexpr.InHypTypeOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >>
- | occs, Tacexpr.InHypValueOnly ->
- <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >>
+ | occs, Termops.InHyp ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >>
+ | occs, Termops.InHypTypeOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >>
+ | occs, Termops.InHypValueOnly ->
+ <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >>
let mlexpr_of_clause cl =
<:expr< {Tacexpr.onhyps=
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a77fc5741..aa6cc297b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -673,10 +673,18 @@ let subst_term_occ (nowhere_except_in,locs as plocs) c t =
if rest <> [] then error_invalid_occurrence rest;
t'
-let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) =
- match bodyopt with
- | None -> (id,None,subst_term_occ plocs c typ)
- | Some body ->
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
+let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
+ match bodyopt,hloc with
+ | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
+ | None, _ -> (id,None,subst_term_occ plocs c typ)
+ | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
+ | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
+ | Some body, InHyp ->
if locs = [] then
if nowhere_except_in then d
else (id,Some (subst_term c body),subst_term c typ)
@@ -687,7 +695,6 @@ let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d
if rest <> [] then error_invalid_occurrence rest;
(id,Some body',t')
-
(* First character of a constr *)
let lowercase_first_char id =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index e9516ec48..92c0a78d4 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -150,8 +150,15 @@ val subst_term_occ : occurrences -> constr -> constr -> constr
(* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
positions [occl] by [Rel 1] in [decl] *)
+
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
val subst_term_occ_decl :
- occurrences -> constr -> named_declaration -> named_declaration
+ occurrences * hyp_location_flag -> constr -> named_declaration ->
+ named_declaration
val error_invalid_occurrence : int list -> 'a
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 29d7a7bb1..b6be71ea0 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -58,12 +58,7 @@ let make_red_flag =
add_flag
{rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
-type hyp_location_flag = (* To distinguish body and type of local defs *)
- | InHyp
- | InHypTypeOnly
- | InHypValueOnly
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
type 'id move_location =
| MoveAfter of 'id
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 80b505a00..6622ccb60 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -131,6 +131,7 @@ open Pattern
open Matching
open Pcoq
open Tacexpr
+open Termops
open Libnames
(* two patterns - one for the type, and one for the type of the type *)
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 89c5e58b8..66b24153a 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -11,6 +11,7 @@
open Tacmach
open Names
open Tacexpr
+open Termops
val instantiate : int -> Rawterm.rawconstr ->
(identifier * hyp_location_flag, unit) location -> tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 158cecfc7..f02ef6dfc 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -16,6 +16,7 @@ open Genarg
open Names
open Tacexpr
open Tacinterp
+open Termops
(* Rewriting orientation *)
@@ -288,7 +289,7 @@ let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause =
Option.map
(fun l ->
List.map
- (fun id -> ( (all_occurrences_expr,trad_id id) ,Tacexpr.InHyp))
+ (fun id -> ( (all_occurrences_expr,trad_id id),InHyp))
l
)
hyps;
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 9369b067f..85ec60078 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -13,6 +13,7 @@ open Term
open Names
open Proof_type
open Topconstr
+open Termops
open Rawterm
val rawwit_orient : bool raw_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d595bfe43..9d73cf75f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -487,13 +487,19 @@ END
TACTIC EXTEND apply_in
| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] ->
- [ apply_in false id cl ]
+ [ apply_in false id cl None ]
+| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id)
+ "as" simple_intropattern(ipat) ] ->
+ [ apply_in false id cl (Some ipat) ]
END
TACTIC EXTEND eapply_in
| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] ->
- [ apply_in true id cl ]
+ [ apply_in true id cl None ]
+| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id)
+ "as" simple_intropattern(ipat) ] ->
+ [ apply_in true id cl (Some ipat) ]
END
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 938befa49..851c33e7a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -1,3 +1,4 @@
+
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -19,6 +20,7 @@ open Tacexpr
open Rawterm
open Evd
open Clenv
+open Termops
(*i*)
(* Tactics for the interpreter. They left a trace in the proof tree
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 87ef65d7c..0186fcb00 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -402,9 +402,26 @@ let rec get_next_hyp_position id = function
else
get_next_hyp_position id right
+let thin_for_replacing l gl =
+ try Tacmach.thin l gl
+ with Evarutil.ClearDependencyError (id,err) -> match err with
+ | Evarutil.OccurHypInSimpleClause None ->
+ errorlabstrm ""
+ (str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion.")
+ | Evarutil.OccurHypInSimpleClause (Some id') ->
+ errorlabstrm ""
+ (str "Cannot change " ++ pr_id id ++
+ strbrk ", it is used in hypothesis " ++ pr_id id' ++ str".")
+ | Evarutil.EvarTypingBreak ev ->
+ errorlabstrm ""
+ (str "Cannot change " ++ pr_id id ++
+ strbrk " without breaking the typing of " ++
+ Printer.pr_existential (pf_env gl) ev ++ str".")
+
let intro_replacing id gl =
let next_hyp = get_next_hyp_position id (pf_hyps gl) in
- tclTHENLIST [thin [id]; introduction id; move_hyp true id next_hyp] gl
+ tclTHENLIST
+ [thin_for_replacing [id]; introduction id; move_hyp true id next_hyp] gl
let intros_replacing ids gl =
let rec introrec = function
@@ -847,12 +864,6 @@ let apply_in_once gl innerclause (d,lbind) =
with NotExtensibleClause -> raise err
in aux (make_clenv_binding gl (d,thm) lbind)
-let apply_in with_evars id lemmas gl =
- let t' = pf_get_hyp_typ gl id in
- let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in
- let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in
- clenv_refine_in with_evars id clause gl
-
(* A useful resolution tactic which, if c:A->B, transforms |- C into
|- B -> C and |- A
@@ -1216,6 +1227,25 @@ let assert_as first ipat c gl =
let assert_tac first na = assert_as first (dloc,ipat_of_name na)
let true_cut = assert_tac true
+(* apply in as *)
+
+let as_tac id ipat = match ipat with
+ | Some (loc,IntroRewrite l2r) ->
+ !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses
+ | Some (loc,IntroOrAndPattern ll) ->
+ intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+ | Some (loc,
+ (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
+ user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
+ | None -> tclIDTAC
+
+let apply_in with_evars id lemmas ipat gl =
+ let t' = pf_get_hyp_typ gl id in
+ let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in
+ let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in
+ tclTHEN (clenv_refine_in with_evars id clause) (as_tac id ipat)
+ gl
+
(**************************)
(* Generalize tactics *)
(**************************)
@@ -1325,10 +1355,10 @@ let out_arg = function
let occurrences_of_hyp id cls =
let rec hyp_occ = function
[] -> None
- | (((b,occs),id'),hl)::_ when id=id' -> Some (b,List.map out_arg occs)
+ | (((b,occs),id'),hl)::_ when id=id' -> Some ((b,List.map out_arg occs),hl)
| _::l -> hyp_occ l in
match cls.onhyps with
- None -> Some (all_occurrences)
+ None -> Some (all_occurrences,InHyp)
| Some l -> hyp_occ l
let occurrences_of_goal cls =
@@ -1395,15 +1425,15 @@ let letin_tac with_eq name c occs gl =
(* Implementation without generalisation: abbrev will be lost in hyps in *)
(* in the extracted proof *)
-let letin_abstract id c occs gl =
+let letin_abstract id c (occs,check_occs) gl =
let env = pf_env gl in
let compute_dependency _ (hyp,_,_ as d) depdecls =
match occurrences_of_hyp hyp occs with
| None -> depdecls
| Some occ ->
let newdecl = subst_term_occ_decl occ c d in
- if occ = all_occurrences & d = newdecl then
- if not (in_every_hyp occs)
+ if occ = (all_occurrences,InHyp) & d = newdecl then
+ if check_occs & not (in_every_hyp occs)
then raise (RefinerError (DoesNotOccurIn (c,hyp)))
else depdecls
else
@@ -1416,7 +1446,7 @@ let letin_abstract id c occs gl =
if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
(depdecls,lastlhyp,ccl)
-let letin_tac with_eq name c ty occs gl =
+let letin_tac_gen with_eq name c ty occs gl =
let id =
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
if name = Anonymous then fresh_id [] x gl else
@@ -1446,7 +1476,10 @@ let letin_tac with_eq name c ty occs gl =
intro_gen dloc (IntroMustBe id) lastlhyp true;
eq_tac;
tclMAP convert_hyp_no_check depdecls ] gl
-
+
+let letin_tac with_eq name c ty occs =
+ letin_tac_gen with_eq name c ty (occs,true)
+
(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
let forward usetac ipat c gl =
match usetac with
@@ -1535,7 +1568,7 @@ let rec first_name_buggy avoid gl (loc,pat) = match pat with
| IntroWildcard -> no_move
| IntroRewrite _ -> no_move
| IntroIdentifier id -> MoveAfter id
- | IntroAnonymous | IntroFresh _ -> assert false
+ | IntroAnonymous | IntroFresh _ -> (* buggy *) no_move
let consume_pattern avoid id gl = function
| [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
@@ -1724,11 +1757,11 @@ let find_atomic_param_of_ind nparams indtyp =
exception Shunt of identifier move_location
-let cook_sign hyp0_opt indvars_init env =
- let hyp0,indvars =
- match hyp0_opt with
- | None -> List.hd (List.rev indvars_init) , indvars_init
- | Some h -> h,indvars_init in
+let cook_sign hyp0_opt indvars env =
+ let hyp0,inhyps =
+ match hyp0_opt with
+ | None -> List.hd (List.rev indvars), []
+ | Some (hyp0,at_least_in_hyps) -> hyp0, at_least_in_hyps in
(* First phase from L to R: get [indhyps], [decldep] and [statuslist]
for the hypotheses before (= more ancient than) hyp0 (see above) *)
let allindhyps = hyp0::indvars in
@@ -1751,9 +1784,9 @@ let cook_sign hyp0_opt indvars_init env =
indhyps := hyp::!indhyps;
rhyp
end else
- if (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps
- or List.exists (fun (id,_,_) -> occur_var_in_decl env id decl)
- !decldeps)
+ if inhyps <> [] && List.mem hyp inhyps || inhyps = [] &&
+ (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps ||
+ List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
then begin
decldeps := decl::!decldeps;
if !before then
@@ -2527,7 +2560,8 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
apply_induction_in_context isrec
None indsign (hyp0::indvars) names induct_tac gl
-let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl =
+let induction_from_context isrec with_evars elim_info (hyp0,lbind) names
+ inhyps gl =
let indsign,scheme = elim_info in
let indref = match scheme.indref with | None -> assert false | Some x -> x in
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -2540,12 +2574,11 @@ let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl =
thin [hyp0]
] in
apply_induction_in_context isrec
- (Some hyp0) indsign indvars names induct_tac gl
-
+ (Some (hyp0,inhyps)) indsign indvars names induct_tac gl
exception TryNewInduct of exn
-let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) gl =
+let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps gl =
let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in
if scheme.indarg = None then (* This is not a standard induction scheme (the
argument is probably a parameter) So try the
@@ -2555,7 +2588,8 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin
let indref = match scheme.indref with | None -> assert false | Some x -> x in
tclTHEN
(atomize_param_of_ind (indref,scheme.nparams) hyp0)
- (induction_from_context isrec with_evars elim_info (hyp0,lbind) names) gl
+ (induction_from_context isrec with_evars elim_info
+ (hyp0,lbind) names inhyps) gl
(* Induction on a list of induction arguments. Analyse the elim
scheme (which is mandatory for multiple ind args), check that all
@@ -2573,26 +2607,65 @@ let induction_without_atomization isrec with_evars elim names lid gl =
then error "Not the right number of induction arguments."
else induction_from_context_l isrec with_evars elim_info lid names gl
+let enforce_eq_name id gl = function
+ | (b,(loc,IntroAnonymous)) ->
+ (b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl)))
+ | (b,(loc,IntroFresh heq_base)) ->
+ (b,(loc,IntroIdentifier (fresh_id [id] heq_base gl)))
+ | x ->
+ x
+
+let clear_unselected_context id inhyps cls gl =
+ match cls with
+ | None -> tclIDTAC gl
+ | Some cls ->
+ let error () =
+ error
+ "Selection of occurrences not supported when destructing a variable."
+ in
+ if occur_var (pf_env gl) id (pf_concl gl) then
+ if cls.concl_occs = no_occurrences_expr then
+ errorlabstrm ""
+ (str "Conclusion must be mentioned: it depends on " ++ pr_id id
+ ++ str ".")
+ else if cls.concl_occs <> all_occurrences_expr then
+ error ();
+ match cls.onhyps with
+ | Some hyps ->
+ List.iter (fun ((occs,id),hl) ->
+ if occs <> all_occurrences_expr || hl <> InHyp then error ()) hyps;
+ let to_erase (id',_,_ as d) =
+ if List.mem id' inhyps then (* if selected, do not erase *) None
+ else
+ (* erase if not selected and dependent on id or selected hyps *)
+ let test id = occur_var_in_decl (pf_env gl) id d in
+ if List.exists test (id::inhyps) then Some id' else None in
+ let ids = list_map_filter to_erase (pf_hyps gl) in
+ thin ids gl
+ | None -> tclIDTAC gl
+
let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
+ let inhyps = match cls with
+ | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
+ | _ -> [] in
match kind_of_term c with
| Var id when not (mem_named_context id (Global.named_context()))
- & lbind = NoBindings & not with_evars & cls = None
- & eqname = None ->
- induction_with_atomization_of_ind_arg
- isrec with_evars elim names (id,lbind) gl
+ & lbind = NoBindings & not with_evars & eqname = None ->
+ tclTHEN
+ (clear_unselected_context id inhyps cls)
+ (induction_with_atomization_of_ind_arg
+ isrec with_evars elim names (id,lbind) inhyps) gl
| _ ->
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
Anonymous in
let id = fresh_id [] x gl in
- let with_eq =
- match eqname with
- | Some eq -> Some (false,eq)
- | _ ->
- if cls <> None then Some (false,(dloc,IntroAnonymous)) else None in
+ (* We need the equality name now *)
+ let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+ (* TODO: if ind has predicate parameters, use JMeq instead of eq *)
tclTHEN
- (letin_tac with_eq (Name id) c None (Option.default allClauses cls))
+ (letin_tac_gen with_eq (Name id) c None (Option.default allClauses cls,false))
(induction_with_atomization_of_ind_arg
- isrec with_evars elim names (id,lbind)) gl
+ isrec with_evars elim names (id,lbind) inhyps) gl
(* Induction on a list of arguments. First make induction arguments
atomic (using letins), then do induction. The specificity here is
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b2bd508ce..589be18c8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -193,7 +193,8 @@ val eapply_with_ebindings : open_constr with_ebindings -> tactic
val cut_and_apply : constr -> tactic
-val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic
+val apply_in : evars_flag -> identifier -> constr with_ebindings list ->
+ intro_pattern_expr located option -> tactic
(*s Elimination tactics. *)
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 633f82edb..a3326ccd3 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -511,7 +511,7 @@ Lemma Nless_trans :
Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
Proof.
induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
- destruct (Nless N0 a'') in *. trivial.
+ destruct (Nless N0 a'') as Heqb in *. trivial.
rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0.
induction a' as [|a' _|a' _] using N_ind_double.
rewrite (Nless_z (Ndouble a)) in H. discriminate H.
@@ -539,10 +539,10 @@ Lemma Nless_total :
forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
Proof.
induction a using N_rec_double; intro a'.
- destruct (Nless N0 a') in *. left. left. auto.
+ destruct (Nless N0 a') as Heqb in *. left. left. auto.
right. rewrite (N0_less_2 a' Heqb). reflexivity.
induction a' as [|a' _|a' _] using N_rec_double.
- destruct (Nless N0 (Ndouble a)) in *. left. right. auto.
+ destruct (Nless N0 (Ndouble a)) as Heqb in *. left. right. auto.
right. exact (N0_less_2 _ Heqb).
rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
left. assumption.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b3d76b89b..e798d8755 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -530,13 +530,13 @@ let compute_bl_tact ind lnamesparrec nparrec =
tclORELSE reflexivity (Equality.discr_tac false None)
);
simpl_in_hyp
- ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
+ ((Rawterm.all_occurrences_expr,freshz),InHyp);
(*
repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
tclREPEAT (
tclTHENSEQ [
- apply_in false freshz [(andb_prop()),Rawterm.NoBindings];
+ apply_in false freshz [(andb_prop()),Rawterm.NoBindings] None;
fun gl ->
let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 18:19:27 +0000