aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml58
-rw-r--r--tactics/class_tactics.mli19
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/hints.ml31
-rw-r--r--tactics/hints.mli3
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/ppred.mli5
-rw-r--r--tactics/tactics.ml287
-rw-r--r--tactics/tactics.mli19
10 files changed, 216 insertions, 219 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1ac7d201a..160e4f164e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -548,7 +548,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
make_apply_entry ~name env sigma flags pri false])
else []
-let make_hints g st only_classes sign =
+let make_hints g (modes,st) only_classes sign =
let hintlist =
List.fold_left
(fun hints hyp ->
@@ -565,7 +565,9 @@ let make_hints g st only_classes sign =
in hint @ hints
else hints)
([]) sign
- in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
+ in
+ let db = Hint_db.add_modes modes @@ Hint_db.empty st true in
+ Hint_db.add_list (pf_env g) (project g) hintlist db
module Search = struct
type autoinfo =
@@ -578,29 +580,29 @@ module Search = struct
(** Local hints *)
let autogoal_cache = Summary.ref ~name:"autogoal_cache"
- (DirPath.empty, true, Context.Named.empty,
+ (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty,
Hint_db.empty TransparentState.full true)
- let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
+ let make_autogoal_hints only_classes (modes,st as mst) g =
let open Proofview in
let open Tacmach.New in
let sign = Goal.hyps g in
- let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
+ let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in
let cwd = Lib.cwd () in
let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in
if DirPath.equal cwd dir &&
(onlyc == only_classes) &&
Context.Named.equal eq sign sign' &&
- Hint_db.transparent_state cached_hints == st
+ cached_modes == modes
then cached_hints
else
let hints = make_hints {it = Goal.goal g; sigma = project g}
- st only_classes sign
+ mst only_classes sign
in
- autogoal_cache := (cwd, only_classes, sign, hints); hints
+ autogoal_cache := (cwd, only_classes, sign, modes, hints); hints
- let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
- let hints = make_autogoal_hints only_classes ~st g in
+ let make_autogoal mst only_classes dep cut i g =
+ let hints = make_autogoal_hints only_classes mst g in
{ search_hints = hints;
search_depth = [i]; last_tac = lazy (str"none");
search_dep = dep;
@@ -695,7 +697,8 @@ module Search = struct
if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
then
let st = Hint_db.transparent_state info.search_hints in
- make_autogoal_hints info.search_only_classes ~st gl'
+ let modes = Hint_db.modes info.search_hints in
+ make_autogoal_hints info.search_only_classes (modes,st) gl'
else info.search_hints
in
let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in
@@ -830,19 +833,19 @@ module Search = struct
(fun e' -> let (e, info) = merge_exceptions e e' in
Proofview.tclZERO ~info e))
- let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
+ let search_tac_gl mst only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
- let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+ let info = make_autogoal mst only_classes dep (cut_of_hints hints) i gl in
search_tac hints depth 1 info
- let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
+ let search_tac mst only_classes dep hints depth =
let open Proofview in
let tac sigma gls i =
Goal.enter
begin fun gl ->
- search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
+ search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end
in
Proofview.Unsafe.tclGETGOALS >>= fun gls ->
let gls = CList.map Proofview.drop_state gls in
@@ -867,11 +870,11 @@ module Search = struct
| (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
- let eauto_tac ?(st=TransparentState.full) ?(unique=false)
+ let eauto_tac mst ?(unique=false)
~only_classes ?strategy ~depth ~dep hints =
let open Proofview in
let tac =
- let search = search_tac ~st only_classes dep hints in
+ let search = search_tac mst only_classes dep hints in
let dfs =
match strategy with
| None -> not (get_typeclasses_iterative_deepening ())
@@ -915,8 +918,8 @@ module Search = struct
| Some i -> str ", with depth limit " ++ int i));
tac
- let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
- Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints
+ let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints =
+ Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints
let run_on_evars env evm p tac =
match evars_to_goals p evm with
@@ -968,8 +971,8 @@ module Search = struct
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
- let evars_eauto env evd depth only_classes unique dep st hints p =
- let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+ let evars_eauto env evd depth only_classes unique dep mst hints p =
+ let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
let res = run_on_evars env evd p eauto_tac in
match res with
| None -> evd
@@ -983,11 +986,11 @@ module Search = struct
let typeclasses_resolve env evd debug depth unique p =
let db = searchtable_map typeclasses_db in
- typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
+ let st = Hint_db.transparent_state db in
+ let modes = Hint_db.modes db in
+ typeclasses_eauto env evd ?depth unique (modes,st) [db] p
end
-(** Binding to either V85 or Search implementations. *)
-
let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
?strategy ~depth dbs =
let dbs = List.map_filter
@@ -996,8 +999,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
dbs
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+ let modes = List.map Hint_db.modes dbs in
+ let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in
let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
- Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
+ Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs
(** We compute dependencies via a union-find algorithm.
Beware of the imperative effects on the partition structure,
@@ -1140,11 +1145,12 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let gls = { it = gl ; sigma = sigma; } in
let hints = searchtable_map typeclasses_db in
let st = Hint_db.transparent_state hints in
+ let modes = Hint_db.modes hints in
let depth = get_typeclasses_depth () in
let gls' =
try
Proofview.V82.of_tactic
- (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
+ (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls
with Refiner.FailError _ -> raise Not_found
in
let evd = sig_sig gls' in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c950e3de3d..b9291f6124 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -27,9 +27,18 @@ type search_strategy = Dfs | Bfs
val set_typeclasses_strategy : search_strategy -> unit
-val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
- depth:(Int.t option) ->
- Hints.hint_db_name list -> unit Proofview.tactic
+val typeclasses_eauto :
+ ?only_classes:bool
+ (** Should non-class goals be shelved and resolved at the end *)
+ -> ?st:TransparentState.t
+ (** The transparent_state used when working with local hypotheses *)
+ -> ?strategy:search_strategy
+ (** Is a traversing-strategy specified? *)
+ -> depth:(Int.t option)
+ (** Bounded or unbounded search *)
+ -> Hints.hint_db_name list
+ (** The list of hint databases to use *)
+ -> unit Proofview.tactic
val head_of_constr : Id.t -> constr -> unit Proofview.tactic
@@ -41,8 +50,8 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig
val eauto_tac :
- ?st:TransparentState.t
- (** The transparent_state used when working with local hypotheses *)
+ Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
+ (** The transparent_state and modes used when working with local hypotheses *)
-> ?unique:bool
(** Should we force a unique solution *)
-> only_classes:bool
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/hints.ml b/tactics/hints.ml
index 11a8816159..cc56c1c425 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -289,8 +289,6 @@ let lookup_tacs sigma concl st se =
let sl' = List.stable_sort pri_order_int l' in
List.merge pri_order_int se.sentry_nopat sl'
-module Constr_map = Map.Make(GlobRef.Ordered)
-
let is_transparent_gr ts = function
| VarRef id -> TransparentState.is_transparent_variable ts id
| ConstRef cst -> TransparentState.is_transparent_constant ts cst
@@ -520,6 +518,8 @@ val add_cut : hints_path -> t -> t
val add_mode : GlobRef.t -> hint_mode array -> t -> t
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
+val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+val modes : t -> hint_mode array list GlobRef.Map.t
val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
t -> 'a -> 'a
@@ -532,7 +532,7 @@ struct
hintdb_unfolds : Id.Set.t * Cset.t;
hintdb_max_id : int;
use_dn : bool;
- hintdb_map : search_entry Constr_map.t;
+ hintdb_map : search_entry GlobRef.Map.t;
(* A list of unindexed entries starting with an unfoldable constant
or with no associated pattern. *)
hintdb_nopat : (GlobRef.t option * stored_data) list;
@@ -548,12 +548,12 @@ struct
hintdb_unfolds = (Id.Set.empty, Cset.empty);
hintdb_max_id = 0;
use_dn = use_dn;
- hintdb_map = Constr_map.empty;
+ hintdb_map = GlobRef.Map.empty;
hintdb_nopat = [];
hintdb_name = name; }
let find key db =
- try Constr_map.find key db.hintdb_map
+ try GlobRef.Map.find key db.hintdb_map
with Not_found -> empty_se
let realize_tac secvars (id,tac) =
@@ -650,11 +650,11 @@ struct
else db
| Some gr ->
let oval = find gr db in
- { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+ { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
let rebuild_db st' db =
let db' =
- { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map;
+ { db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map;
hintdb_state = st'; hintdb_nopat = [] }
in
List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
@@ -693,7 +693,7 @@ struct
let remove_list grs db =
let filter (_, h) =
match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
- let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
+ let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map in
let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
@@ -706,11 +706,11 @@ struct
let iter f db =
let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
- Constr_map.iter iter_se db.hintdb_map
+ GlobRef.Map.iter iter_se db.hintdb_map
let fold f db accu =
let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
- Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
+ GlobRef.Map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
let transparent_state db = db.hintdb_state
@@ -724,12 +724,21 @@ struct
let add_mode gr m db =
let se = find gr db in
let se = { se with sentry_mode = m :: se.sentry_mode } in
- { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
+ { db with hintdb_map = GlobRef.Map.add gr se db.hintdb_map }
let cut db = db.hintdb_cut
let unfolds db = db.hintdb_unfolds
+ let add_modes modes db =
+ let f gr e me =
+ Some { e with sentry_mode = me.sentry_mode @ e.sentry_mode }
+ in
+ let mode_entries = GlobRef.Map.map (fun m -> { empty_se with sentry_mode = m }) modes in
+ { db with hintdb_map = GlobRef.Map.union f db.hintdb_map mode_entries }
+
+ let modes db = GlobRef.Map.map (fun se -> se.sentry_mode) db.hintdb_map
+
let use_dn db = db.use_dn
end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 90a8b7fe52..7b8f96cdd8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -162,6 +162,9 @@ module Hint_db :
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
+
+ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+ val modes : t -> hint_mode array list GlobRef.Map.t
end
type hint_db = Hint_db.t
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 b70dd63211..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,15 +802,21 @@ 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 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 -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ | None ->
+ if check then
+ change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ else
+ t Id.Map.empty env sigma
| Some occl ->
e_contextually false occl
(fun subst ->
- change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
- env sigma c in
+ if check then
+ change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
+ else
+ fun env sigma _c -> t subst env sigma) env sigma c in
if !mayneedglobalcheck then
begin
try ignore (Typing.unsafe_type_of env sigma c)
@@ -819,14 +825,13 @@ let change_on_subterm cv_pb deep t where env sigma c =
end;
(sigma, c)
-let change_in_concl occl t =
- e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+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)
-let change_in_hyp 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:true (fun x -> change_on_subterm 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 ->
@@ -835,43 +840,44 @@ 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 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
| NoOccurrences -> Proofview.tclUNIT ()
- | occs -> change_in_concl (bind_change_occurrences occs chg) c
+ | occs -> change_in_concl ~check (bind_change_occurrences occs chg) c
end
<*>
let f (id, occs, where) =
let occl = bind_change_occurrences occs chg in
- let redfun deep env sigma t = change_on_subterm 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:true 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 None (make_change_arg 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 *)
@@ -886,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 ->
@@ -900,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
@@ -1295,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;
@@ -1314,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)
(********************************************)
@@ -1353,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
@@ -1380,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
@@ -1392,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 =
@@ -1401,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
@@ -1429,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) =
@@ -1461,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
@@ -1482,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 =
@@ -1508,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 =
@@ -1821,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 ->
@@ -1842,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;
@@ -1859,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
@@ -2486,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
@@ -2554,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 =
@@ -2586,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 *)
@@ -2647,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
@@ -2856,17 +2834,21 @@ let generalize_dep ?(with_let=false) c =
| _ -> tothin
in
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
- let body =
- if with_let then
- match EConstr.kind sigma c with
- | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
- | _ -> None
- else None
+ let is_var, body = match EConstr.kind sigma c with
+ | Var id ->
+ let body = NamedDecl.get_value (pf_get_hyp id gl) in
+ let is_var = Option.is_empty body && not (List.mem id init_ids) in
+ if with_let then is_var, body else is_var, None
+ | _ -> false, None
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
(* Check that the generalization is indeed well-typed *)
- let (evd, _) = Typing.type_of env evd cl'' in
+ let evd =
+ (* No need to retype for variables, term is statically well-typed *)
+ if is_var then evd
+ else fst (Typing.type_of env evd cl'')
+ in
let args = Context.Named.to_instance mkVar to_quantify_rev in
tclTHENLIST
[ Proofview.Unsafe.tclEVARS evd;
@@ -3050,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
@@ -3280,7 +3262,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
if Int.equal i nparams then
let t = applist (hd, params@args) in
Tacticals.New.tclTHEN
- (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
+ (change_in_hyp ~check:false None (make_change_arg t) (hyp0,InHypTypeOnly))
(tac avoid)
else
let c = List.nth argl (i-1) in
@@ -4172,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
@@ -4199,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
@@ -4246,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
@@ -4351,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 e7b95a820e..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 : (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 : (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 :
- 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-03 02:15:59 +0000