aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/ind_tables.ml20
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/ppred.mli5
-rw-r--r--tactics/tactics.ml250
-rw-r--r--tactics/tactics.mli19
8 files changed, 135 insertions, 174 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 7a61deba0c..499152f39a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -174,7 +174,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let lem = mkConstU (cst, inst) in
let evd = Evd.set_universe_context evd ectx in
let open Safe_typing in
- let eff = private_con_of_con (Global.safe_env ()) cst in
+ let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in
let effs = concat_private eff
Entries.(snd (Future.force const.const_entry_body)) in
let solve =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 70854e6e3c..0857c05968 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -514,7 +514,7 @@ let autounfold_one db cl =
in
if did then
match cl with
- | Some hyp -> change_in_hyp None (make_change_arg c') hyp
+ | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
| None -> convert_concl ~check:false c' DEFAULTcast
else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3d760f1c3d..45a4799ea1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
- {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
+ {elimindex = None; elimbody = (elim,NoBindings) }
end
let adjust_rewriting_direction args lft2rgt =
@@ -1613,10 +1613,10 @@ let cutSubstInHyp l2r eqn id =
tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(tclTHENFIRST
(tclTHENLIST [
- (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
+ (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly));
(replace_core (onHyp id) l2r eqn)
])
- (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+ (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly)))
end
let try_rewrite tac =
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 16829482e5..e95778a90d 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -147,9 +147,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
+ let role = Entries.Schema (ind, kind) in
+ let neff = Safe_typing.private_constant (Global.safe_env ()) role const in
declare_scheme kind [|ind,const|];
- const, Safe_typing.concat_private
- (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
+ const, Safe_typing.concat_private neff eff
let define_individual_scheme kind mode names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
@@ -163,15 +164,16 @@ let define_mutual_scheme_base kind suff f mode names mind =
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
- let consts = Array.map2 (fun id cl ->
- define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
+ let fold i effs id cl =
+ let cst = define mode id cl (Declareops.inductive_is_polymorphic mib) ctx in
+ let role = Entries.Schema ((mind, i), kind)in
+ let neff = Safe_typing.private_constant (Global.safe_env ()) role cst in
+ (Safe_typing.concat_private neff effs, cst)
+ in
+ let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
declare_scheme kind schemes;
- consts,
- Safe_typing.concat_private
- (Safe_typing.private_con_of_scheme
- ~kind (Global.safe_env()) (Array.to_list schemes))
- eff
+ consts, eff
let define_mutual_scheme kind mode names mind =
match Hashtbl.find scheme_object_table kind with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4aa4d13e1e..6efa1ece9c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
(str"Computed inversion goal was not closed in initial signature.");
*)
let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
- let pf =
- fst (Proof.run_tactic env (
- tclTHEN intro (onLastHypId inv_op)) pf)
- in
+ let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
let pfterm = List.hd (Proof.partial_proof pf) in
let global_named_context = Global.named_context_val () in
let ownSign = ref begin
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
index be21236f4e..c68fab5296 100644
--- a/tactics/ppred.mli
+++ b/tactics/ppred.mli
@@ -6,11 +6,6 @@ val pr_with_occurrences :
val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
-val pr_red_expr :
- ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
- (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
- [@@ocaml.deprecated "Use pr_red_expr_env instead"]
-
val pr_red_expr_env : Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
(Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e8869f9b0..2bdfc85d6d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -145,7 +145,7 @@ let introduction id =
let error msg = CErrors.user_err Pp.(str msg)
-let convert_concl ?(check=true) ty k =
+let convert_concl ~check ty k =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let conclty = Proofview.Goal.concl gl in
@@ -163,12 +163,12 @@ let convert_concl ?(check=true) ty k =
end
end
-let convert_hyp ?(check=true) d =
+let convert_hyp ~check ~reorder d =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let sign = convert_hyp check (named_context_val env) sigma d in
+ let sign = convert_hyp ~check ~reorder env sigma d in
let env = reset_with_named_context sign env in
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ty
@@ -176,7 +176,7 @@ let convert_hyp ?(check=true) d =
end
let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false
+let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
@@ -701,7 +701,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
(** Tactic reduction modulo evars (for universes essentially) *)
-let e_change_in_concl ?(check = false) (redfun, sty) =
+let e_change_in_concl ~check (redfun, sty) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -709,16 +709,16 @@ let e_change_in_concl ?(check = false) (redfun, sty) =
(convert_concl ~check c' sty)
end
-let e_change_in_hyp ?(check = false) redfun (id,where) =
+let e_change_in_hyp ~check ~reorder redfun (id,where) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let hyp = Tacmach.New.pf_get_hyp id gl in
let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (convert_hyp ~check c)
+ (convert_hyp ~check ~reorder c)
end
-let e_change_in_hyps ?(check=true) f args =
+let e_change_in_hyps ~check ~reorder f args =
Proofview.Goal.enter begin fun gl ->
let fold (env, sigma) arg =
let (redfun, id, where) = f arg in
@@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args =
raise (RefinerError (env, sigma, NoSuchHyp id))
in
let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
- let sign = Logic.convert_hyp check (named_context_val env) sigma d in
+ let sign = Logic.convert_hyp ~check ~reorder env sigma d in
let env = reset_with_named_context sign env in
(env, sigma)
in
@@ -745,26 +745,26 @@ let e_change_in_hyps ?(check=true) f args =
let e_reduct_in_concl = e_change_in_concl
-let reduct_in_concl ?(check = false) (redfun, sty) =
+let reduct_in_concl ~check (redfun, sty) =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_change_in_concl ~check (redfun, sty)
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_reduct_in_hyp ~check ~reorder redfun (id, where) =
let redfun _ env sigma c = redfun env sigma c in
- e_change_in_hyp ~check redfun (id, where)
+ e_change_in_hyp ~check ~reorder redfun (id, where)
-let reduct_in_hyp ?(check = false) redfun (id, where) =
+let reduct_in_hyp ~check ~reorder redfun (id, where) =
let redfun _ env sigma c = (sigma, redfun env sigma c) in
- e_change_in_hyp ~check redfun (id, where)
+ e_change_in_hyp ~check ~reorder redfun (id, where)
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
-let e_reduct_option ?(check=false) redfun = function
- | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+let e_reduct_option ~check redfun = function
+ | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id
| None -> e_change_in_concl ~check (revert_cast redfun)
-let reduct_option ?(check = false) (redfun, sty) where =
+let reduct_option ~check (redfun, sty) where =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_reduct_option ~check (redfun, sty) where
@@ -802,7 +802,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
| Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm check cv_pb deep t where env sigma c =
+let change_on_subterm ~check cv_pb deep t where env sigma c =
let mayneedglobalcheck = ref false in
let (sigma, c) = match where with
| None ->
@@ -825,15 +825,13 @@ let change_on_subterm check cv_pb deep t where env sigma c =
end;
(sigma, c)
-let change_in_concl ?(check=true) occl t =
+let change_in_concl ~check occl t =
(* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
- e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
+ e_change_in_concl ~check:false ((change_on_subterm ~check Reduction.CUMUL false t occl),DEFAULTcast)
-let change_in_hyp ?(check=true) occl t id =
- (* FIXME: we set the [check] flag only to reorder hypotheses in case of
- introduction of dependencies in new variables. We should separate this
- check from the conversion function. *)
- e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id
+let change_in_hyp ~check occl t id =
+ (* Same as above *)
+ e_change_in_hyp ~check:false ~reorder:check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -842,7 +840,7 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with
| Some l ->
List.map (fun ((occs, id), w) -> (id, occs, w)) l
-let change ?(check=true) chg c cls =
+let change ~check chg c cls =
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
begin match cls.concl_occs with
@@ -852,33 +850,34 @@ let change ?(check=true) chg c cls =
<*>
let f (id, occs, where) =
let occl = bind_change_occurrences occs chg in
- let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
+ let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
- e_change_in_hyps ~check f hyps
+ (* Don't check, we do it already in [change_on_subterm] *)
+ e_change_in_hyps ~check:false ~reorder:check f hyps
end
let change_concl t =
change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let red_in_concl = reduct_in_concl (red_product,REVERTcast)
-let red_in_hyp = reduct_in_hyp red_product
-let red_option = reduct_option (red_product,REVERTcast)
-let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast)
-let hnf_in_hyp = reduct_in_hyp hnf_constr
-let hnf_option = reduct_option (hnf_constr,REVERTcast)
-let simpl_in_concl = reduct_in_concl (simpl,REVERTcast)
-let simpl_in_hyp = reduct_in_hyp simpl
-let simpl_option = reduct_option (simpl,REVERTcast)
-let normalise_in_concl = reduct_in_concl (compute,REVERTcast)
-let normalise_in_hyp = reduct_in_hyp compute
-let normalise_option = reduct_option (compute,REVERTcast)
-let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
-let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
-let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
-let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
+let red_in_concl = reduct_in_concl ~check:false (red_product,REVERTcast)
+let red_in_hyp = reduct_in_hyp ~check:false ~reorder:false red_product
+let red_option = reduct_option ~check:false (red_product,REVERTcast)
+let hnf_in_concl = reduct_in_concl ~check:false (hnf_constr,REVERTcast)
+let hnf_in_hyp = reduct_in_hyp ~check:false ~reorder:false hnf_constr
+let hnf_option = reduct_option ~check:false (hnf_constr,REVERTcast)
+let simpl_in_concl = reduct_in_concl ~check:false (simpl,REVERTcast)
+let simpl_in_hyp = reduct_in_hyp ~check:false ~reorder:false simpl
+let simpl_option = reduct_option ~check:false (simpl,REVERTcast)
+let normalise_in_concl = reduct_in_concl ~check:false (compute,REVERTcast)
+let normalise_in_hyp = reduct_in_hyp ~check:false ~reorder:false compute
+let normalise_option = reduct_option ~check:false (compute,REVERTcast)
+let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast)
+let unfold_in_hyp loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname)
+let unfold_option loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast)
+let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast)
(* The main reduction function *)
@@ -893,6 +892,7 @@ let reduce redexp cl =
let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in
let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
+ let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in
begin match cl.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
| occs ->
@@ -907,7 +907,7 @@ let reduce redexp cl =
let redfun _ env sigma c = redfun env sigma c in
(redfun, id, where)
in
- e_change_in_hyps ~check f hyps
+ e_change_in_hyps ~check ~reorder f hyps
end
end
@@ -1302,14 +1302,11 @@ let do_replace id = function
[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)
- targetid id sigma0 clenv tac =
+let clenv_refine_in with_evars targetid id sigma0 clenv tac =
let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
- if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses
~fail:(not with_evars) clenv.env clenv.evd }
- else clenv
in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
@@ -1321,11 +1318,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
- (if sidecond_first then
- Tacticals.New.tclTHENFIRST
- (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
- else
- Tacticals.New.tclTHENLAST
+ (Tacticals.New.tclTHENLAST
(assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
(********************************************)
@@ -1360,22 +1353,25 @@ let rec contract_letin_in_lam_header sigma c =
| LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c)
| _ -> c
-let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ())
- rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let elim = contract_letin_in_lam_header sigma elim in
- let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
- let indmv =
- (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
- | Meta mv -> mv
- | _ -> user_err ~hdr:"elimination_clause"
- (str "The type of elimination clause is not well-formed."))
+let elimination_in_clause_scheme env sigma with_evars ~flags
+ id hypmv elimclause =
+ let hyp = mkVar id in
+ let hyp_typ = Retyping.get_type_of env sigma hyp in
+ let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
+ let elimclause'' =
+ (* The evarmap of elimclause is assumed to be an extension of hypclause, so
+ we do not need to merge the universes coming from hypclause. *)
+ try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause
+ with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
+ (* Set the hypothesis name in the message *)
+ raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
in
- let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
- end
+ let new_hyp_typ = clenv_type elimclause'' in
+ if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
+ user_err ~hdr:"general_rewrite_in"
+ (str "Nothing to rewrite in " ++ Id.print id ++ str".");
+ clenv_refine_in with_evars id id sigma elimclause''
+ (fun id -> Proofview.tclUNIT ())
(*
* Elimination tactic with bindings and using an arbitrary
@@ -1387,11 +1383,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
type eliminator = {
elimindex : int option; (* None = find it automatically *)
- elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
elimbody : EConstr.constr with_bindings
}
-let general_elim_clause_gen elimtac indclause elim =
+let general_elim_clause with_evars flags where indclause elim =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -1399,7 +1394,27 @@ let general_elim_clause_gen elimtac indclause elim =
let elimt = Retyping.get_type_of env sigma elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
- elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
+ let elimc = contract_letin_in_lam_header sigma elimc in
+ let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in
+ let indmv =
+ (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
+ | Meta mv -> mv
+ | _ -> user_err ~hdr:"elimination_clause"
+ (str "The type of elimination clause is not well-formed."))
+ in
+ match where with
+ | None ->
+ let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+ Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags
+ | Some id ->
+ let hypmv =
+ match List.remove Int.equal indmv (clenv_independent elimclause) with
+ | [a] -> a
+ | _ -> user_err ~hdr:"elimination_clause"
+ (str "The type of elimination clause is not well-formed.")
+ in
+ let elimclause = clenv_fchain ~flags indmv elimclause indclause in
+ elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause
end
let general_elim with_evars clear_flag (c, lbindc) elim =
@@ -1408,12 +1423,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
let sigma = Tacmach.New.project gl in
let ct = Retyping.get_type_of env sigma c in
let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
- let elimtac = elimination_clause_scheme with_evars in
let indclause = make_clenv_binding env sigma (c, t) lbindc in
let sigma = meta_merge sigma (clear_metas indclause.evd) in
+ let flags = elim_flags () in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.New.tclTHEN
- (general_elim_clause_gen elimtac indclause elim)
+ (general_elim_clause with_evars flags None indclause elim)
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
end
@@ -1436,8 +1451,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
let elim = EConstr.of_constr elim in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(general_elim with_evars clear_flag (c,lbindc)
- {elimindex = None; elimbody = (elim,NoBindings);
- elimrename = Some (false, constructors_nrealdecls env (fst mind))})
+ {elimindex = None; elimbody = (elim,NoBindings); })
end
let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1468,8 +1482,7 @@ let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
if is_nonrec ind then raise IsNonrec;
let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
- evd, {elimindex = None; elimbody = (c,NoBindings);
- elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)}
+ evd, { elimindex = None; elimbody = (c,NoBindings) }
let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
@@ -1489,7 +1502,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
let elim_in_context with_evars clear_flag c = function
| Some elim ->
general_elim with_evars clear_flag c
- {elimindex = Some (-1); elimbody = elim; elimrename = None}
+ { elimindex = Some (-1); elimbody = elim }
| None -> default_elim with_evars clear_flag c
let elim with_evars clear_flag (c,lbindc as cx) elim =
@@ -1515,48 +1528,6 @@ let simplest_elim c = default_elim false None (c,NoBindings)
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
-let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
- (* The evarmap of elimclause is assumed to be an extension of hypclause, so
- we do not need to merge the universes coming from hypclause. *)
- try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
- with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
- (* Set the hypothesis name in the message *)
- raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
- id rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let elim = contract_letin_in_lam_header sigma elim in
- let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
- let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
- let hypmv =
- match List.remove Int.equal indmv (clenv_independent elimclause) with
- | [a] -> a
- | _ -> user_err ~hdr:"elimination_clause"
- (str "The type of elimination clause is not well-formed.")
- in
- let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- let hyp = mkVar id in
- let hyp_typ = Retyping.get_type_of env sigma hyp in
- let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
- let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
- let new_hyp_typ = clenv_type elimclause'' in
- if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
- user_err ~hdr:"general_rewrite_in"
- (str "Nothing to rewrite in " ++ Id.print id ++ str".");
- clenv_refine_in with_evars id id sigma elimclause''
- (fun id -> Proofview.tclUNIT ())
- end
-
-let general_elim_clause with_evars flags id c e =
- let elim = match id with
- | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags
- | Some id -> elimination_in_clause_scheme with_evars ~flags id
- in
- general_elim_clause_gen elim c e
-
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
@@ -1828,7 +1799,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
in
aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_once ?(respect_opaque = false) with_delta
with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
@@ -1849,7 +1820,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
- clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
+ clenv_refine_in with_evars targetid id sigma clause
(fun id ->
Tacticals.New.tclTHENLIST [
apply_clear_request clear_flag false c;
@@ -1866,14 +1837,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
aux [] with_destruct d
end
-let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+let apply_in_delayed_once ?(respect_opaque = false) with_delta
with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
- (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
+ (apply_in_once ~respect_opaque with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
end
@@ -2493,7 +2464,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
clear [id] in
let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
in
- apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f)
+ apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f)
(fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
and prepare_intros ?loc with_evars dft destopt = function
@@ -2561,10 +2532,10 @@ let assert_as first hd ipat t =
(* apply in as *)
-let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+let general_apply_in ?(respect_opaque=false) with_delta
with_destruct with_evars id lemmas ipat =
let tac (naming,lemma) tac id =
- apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+ apply_in_delayed_once ~respect_opaque with_delta
with_destruct with_evars naming id lemma tac in
Proofview.Goal.enter begin fun gl ->
let destopt =
@@ -2593,10 +2564,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
let apply_in simple with_evars id lemmas ipat =
let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
- general_apply_in false simple simple with_evars id lemmas ipat
+ general_apply_in simple simple with_evars id lemmas ipat
let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
+ general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
@@ -2654,7 +2625,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
[ Proofview.Unsafe.tclEVARS sigma;
convert_concl ~check:false newcl DEFAULTcast;
intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
- Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls;
+ Tacticals.New.tclMAP (convert_hyp ~check:false ~reorder:false) depdecls;
eq_tac ]
end
@@ -3061,8 +3032,8 @@ let unfold_body x =
Tacticals.New.afterHyp x begin fun aft ->
let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
let rfun _ _ c = replace_vars [x, xval] c in
- let reducth h = reduct_in_hyp rfun h in
- let reductc = reduct_in_concl (rfun, DEFAULTcast) in
+ let reducth h = reduct_in_hyp ~check:false ~reorder:false rfun h in
+ let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in
Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
end
end
@@ -4183,7 +4154,7 @@ let find_induction_type isrec elim hyp0 gl =
let scheme = compute_elim_sig sigma ~elimc elimt in
if Option.is_empty scheme.indarg then error "Cannot find induction type";
let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
- let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
+ let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
scheme, ElimUsing (elim,indsign)
in
match scheme.indref with
@@ -4210,10 +4181,7 @@ let get_eliminator elim dep s gl =
| ElimOver (isrec,id) ->
let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
let _, (l, s) = compute_elim_signature elims id in
- let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
- (List.rev s.branches)
- in
- evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
+ evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l
(* Instantiate all meta variables of elimclause using lid, some elts
of lid are parameters (first ones), the other are
@@ -4257,7 +4225,7 @@ let recolle_clenv i params args elimclause gl =
let induction_tac with_evars params indvars elim =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
- let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
+ let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in
let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
let elimc = contract_letin_in_lam_header sigma elimc in
@@ -4362,7 +4330,7 @@ let induction_without_atomization isrec with_evars elim names lid =
(* FIXME: Tester ca avec un principe dependant et non-dependant *)
induction_tac with_evars params realindvars elim;
] in
- let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
+ let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in
apply_induction_in_context with_evars None [] elim indvars names induct_tac
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b3914816ac..32c64bacf6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -33,8 +33,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
(** {6 Primitive tactics. } *)
val introduction : Id.t -> unit Proofview.tactic
-val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
[@@ocaml.deprecated "use [Tactics.convert_concl]"]
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
@@ -152,13 +152,13 @@ type e_tactic_reduction = Reductionops.e_reduction_function
type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
val make_change_arg : constr -> change_arg
-val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
-val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_option : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
+val reduct_in_concl : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
+val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val change_in_concl : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : constr -> unit Proofview.tactic
-val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp : check:bool -> (occurrences * constr_pattern) option -> change_arg ->
hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : hyp_location -> unit Proofview.tactic
@@ -180,7 +180,7 @@ val unfold_in_hyp :
val unfold_option :
(occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
val change :
- ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+ check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
@@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_
(** elim principle with the index of its inductive arg *)
type eliminator = {
elimindex : int option; (** None = find it automatically *)
- elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
elimbody : constr with_bindings
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:36:25 +0000