aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/cbn.ml60
-rw-r--r--tactics/class_tactics.ml3
-rw-r--r--tactics/declareUctx.ml2
-rw-r--r--tactics/eauto.ml1
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/eqschemes.ml40
-rw-r--r--tactics/equality.ml3
-rw-r--r--tactics/genredexpr.ml17
-rw-r--r--tactics/hints.ml27
-rw-r--r--tactics/hints.mli6
-rw-r--r--tactics/redexpr.ml116
-rw-r--r--tactics/redexpr.mli13
-rw-r--r--tactics/tactics.ml162
-rw-r--r--tactics/tactics.mli6
-rw-r--r--tactics/term_dnet.ml5
16 files changed, 253 insertions, 216 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 369508c2a3..353e138599 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -277,8 +277,8 @@ let hintmap_of env sigma secvars hdc concl =
else Hint_db.map_auto env sigma ~secvars hdc concl
let exists_evaluable_reference env = function
- | EvalConstRef _ -> true
- | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
+ | Tacred.EvalConstRef _ -> true
+ | Tacred.EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro
let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 31873ea6b0..39959d6fb8 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -104,9 +104,11 @@ sig
| Cst_const of pconstant
| Cst_proj of Projection.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+ | Case of 'a case_stk * Cst_stack.t
| Proj of Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -121,7 +123,7 @@ sig
val append_app : 'a array -> 'a t -> 'a t
val decomp : 'a t -> ('a * 'a t) option
val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
- -> 'a t -> 'a t -> bool
+ -> ('a case_stk -> 'a case_stk -> bool) -> 'a t -> 'a t -> bool
val strip_app : 'a t -> 'a t * 'a t
val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
val will_expose_iota : 'a t -> bool
@@ -156,9 +158,11 @@ struct
| Cst_const of pconstant
| Cst_proj of Projection.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+ | Case of 'a case_stk * Cst_stack.t
| Proj of Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -172,9 +176,9 @@ struct
let pr_c x = hov 1 (pr_c x) in
match member with
| App app -> str "ZApp" ++ pr_app_node pr_c app
- | Case (_,_,_,br,cst) ->
+ | Case ((_,_,_,_,_,br),cst) ->
str "ZCase(" ++
- prvect_with_sep (pr_bar) pr_c br
+ prvect_with_sep (pr_bar) (fun (_, b) -> pr_c b) br
++ str ")"
| Proj (p,cst) ->
str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -221,7 +225,7 @@ struct
if i < j then (l.(j), App (i,l,pred j) :: sk)
else (l.(j), sk)
- let equal f f_fix sk1 sk2 =
+ let equal f f_fix f_case sk1 sk2 =
let equal_cst_member x y =
match x, y with
| Cst_const (c1,u1), Cst_const (c2, u2) ->
@@ -236,8 +240,8 @@ struct
let t1,s1' = decomp_node_last a1 s1 in
let t2,s2' = decomp_node_last a2 s2 in
(f t1 t2) && (equal_rec s1' s2')
- | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
- f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
+ | Case ((ci1,pms1,p1,t1,iv1,a1),_) :: s1, Case ((ci2,pms2,p2,iv2,t2,a2),_) :: s2 ->
+ f_case (ci1,pms1,p1,t1,iv1,a1) (ci2,pms2,p2,iv2,t2,a2) && equal_rec s1 s2
| (Proj (p,_)::s1, Proj(p2,_)::s2) ->
Projection.Repr.CanOrd.equal (Projection.repr p) (Projection.repr p2)
&& equal_rec s1 s2
@@ -284,7 +288,7 @@ struct
let will_expose_iota args =
List.exists
- (function (Fix (_,_,l) | Case (_,_,_,_,l) |
+ (function (Fix (_,_,l) | Case (_,l) |
Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
args
@@ -346,9 +350,9 @@ struct
then a
else Array.sub a i (j - i + 1) in
zip (mkApp (f, a'), s)
- | f, (Case (ci,rt,iv,br,cst_l)::s) when refold ->
- zip (best_state sigma (mkCase (ci,rt,iv,f,br), s) cst_l)
- | f, (Case (ci,rt,iv,br,_)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+ | f, (Case ((ci,u,pms,rt,iv,br),cst_l)::s) when refold ->
+ zip (best_state sigma (mkCase (ci,u,pms,rt,iv,f,br), s) cst_l)
+ | f, (Case ((ci,u,pms,rt,iv,br),_)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
| f, (Fix (fix,st,cst_l)::s) when refold ->
zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
| f, (Fix (fix,st,_)::s) -> zip
@@ -533,7 +537,26 @@ let debug_RAKAM = Reductionops.debug_RAKAM
let equal_stacks sigma (x, l) (y, l') =
let f_equal x y = eq_constr sigma x y in
let eq_fix a b = f_equal (mkFix a) (mkFix b) in
- Stack.equal f_equal eq_fix l l' && f_equal x y
+ let eq_case (ci1, u1, pms1, p1, _, br1) (ci2, u2, pms2, p2, _, br2) =
+ Array.equal f_equal pms1 pms2 &&
+ f_equal (snd p1) (snd p2) &&
+ Array.equal (fun (_, c1) (_, c2) -> f_equal c1 c2) br1 br2
+ in
+ Stack.equal f_equal eq_fix eq_case l l' && f_equal x y
+
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+ let args = Stack.tail ci.ci_npar args in
+ let args = Option.get (Stack.list_of_app_stack args) in
+ let br = lf.(i - 1) in
+ let subst =
+ if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+ (* No let-bindings *)
+ List.rev args
+ else
+ let ctx = expand_branch env sigma u pms (ind, i) br in
+ subst_of_rel_context_instance ctx args
+ in
+ Vars.substl subst (snd br)
let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
@@ -699,8 +722,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| _ -> fold ())
| _ -> fold ())
- | Case (ci,p,iv,d,lf) ->
- whrec Cst_stack.empty (d, Stack.Case (ci,p,iv,lf,cst_l) :: stack)
+ | Case (ci,u,pms,p,iv,d,lf) ->
+ whrec Cst_stack.empty (d, Stack.Case ((ci,u,pms,p,iv,lf),cst_l) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -708,13 +731,14 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
|Some (bef,arg,s') ->
whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
- | Construct ((ind,c),u) ->
+ | Construct (cstr ,u) ->
let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
if use_match || use_fix then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, _, lf,_)::s') when use_match ->
- whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+ |args, (Stack.Case(case,_)::s') when use_match ->
+ let r = apply_branch env sigma cstr args case in
+ whrec Cst_stack.empty (r, s')
|args, (Stack.Proj (p,_)::s') when use_match ->
whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9e66e8668f..d93501eea6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1014,10 +1014,11 @@ let deps_of_constraints cstrs evm p =
cstrs
let evar_dependencies pred evm p =
+ let cache = Evarutil.create_undefined_evars_cache () in
Evd.fold_undefined
(fun ev evi _ ->
if Evd.is_typeclass_evar evm ev && pred evm ev evi then
- let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+ let evars = Evar.Set.add ev (Evarutil.filtered_undefined_evars_of_evar_info ~cache evm evi)
in Intpart.union_set evars p
else ())
evm ()
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
index bca43697cb..6c8bc92865 100644
--- a/tactics/declareUctx.ml
+++ b/tactics/declareUctx.ml
@@ -16,7 +16,7 @@ let name_instance inst =
assert false
| Some na ->
try
- let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in
+ let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in
Names.Name (Libnames.qualid_basename qid)
with Not_found ->
(* Best-effort naming from the string representation of the level.
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e920093648..20c557b282 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -386,6 +386,7 @@ let make_dimension n = function
| Some d -> (false,d)
let autounfolds ids csts gl cls =
+ let open Tacred in
let hyps = Tacmach.New.pf_ids_of_hyps gl in
let env = Tacmach.New.pf_env gl in
let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d4cc193eb3..9b3f9053cd 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -123,8 +123,8 @@ let idy = Id.of_string "y"
let mkGenDecideEqGoal rectype ops g =
let hypnames = pf_ids_set_of_hyps g in
- let xname = next_ident_away idx hypnames
- and yname = next_ident_away idy hypnames in
+ let xname = next_ident_away idx hypnames in
+ let yname = next_ident_away idy (Id.Set.add xname hypnames) in
(mkNamedProd (make_annot xname Sorts.Relevant) rectype
(mkNamedProd (make_annot yname Sorts.Relevant) rectype
(mkDecideEqGoal true ops
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f90c143a1a..54e9a87c96 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -216,7 +216,7 @@ let build_sym_scheme env ind =
let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkApp (mkIndU indu,Array.concat
@@ -225,7 +225,7 @@ let build_sym_scheme env ind =
rel_vect (2*nrealargs+2) nrealargs])),
NoInvert,
mkRel 1 (* varH *),
- [|cstr (nrealargs+1)|]))))
+ [|cstr (nrealargs+1)|])))))
in c, UState.of_context_set ctx
let sym_scheme_kind =
@@ -279,13 +279,13 @@ let build_sym_involutive_scheme env ind =
let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
- (mkCase (ci,
- my_it_mkLambda_or_LetIn_name
- (lift_rel_context (nrealargs+1) realsign_ind)
- (mkApp (eq,[|
- mkApp
- (mkIndU indu, Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ (mkCase (Inductive.contract_case env (ci,
+ my_it_mkLambda_or_LetIn_name
+ (lift_rel_context (nrealargs+1) realsign_ind)
+ (mkApp (eq,[|
+ mkApp
+ (mkIndU indu, Array.concat
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
rel_vect (2*nrealargs+2) nrealargs;
rel_vect 1 nrealargs]);
mkApp (sym,Array.concat
@@ -300,7 +300,7 @@ let build_sym_involutive_scheme env ind =
mkRel 1|])),
NoInvert,
mkRel 1 (* varH *),
- [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+ [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
in (c, UState.of_context_set ctx)
let sym_involutive_scheme_kind =
@@ -437,11 +437,11 @@ let build_l2r_rew_scheme dep env ind kind =
rel_vect 4 nrealargs;
[|mkRel 2|]])|]]) in
let main_body =
- mkCase (ci,
+ mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
NoInvert,
applied_sym_C 3,
- [|mkVar varHC|])
+ [|mkVar varHC|]))
in
let c =
(my_it_mkLambda_or_LetIn paramsctxt
@@ -451,7 +451,7 @@ let build_l2r_rew_scheme dep env ind kind =
(mkNamedLambda (make_annot varHC indr) applied_PC
(mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
(if dep then (* we need a coercion *)
- mkCase (cieq,
+ mkCase (Inductive.contract_case env (cieq,
mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
mkLambda (make_annot Anonymous indr,
mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
@@ -459,7 +459,7 @@ let build_l2r_rew_scheme dep env ind kind =
NoInvert,
mkApp (sym_involutive,
Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
- [|main_body|])
+ [|main_body|]))
else
main_body))))))
in (c, UState.of_context_set ctx)
@@ -540,7 +540,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign
(mkNamedLambda (make_annot varH indr) applied_ind
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkNamedProd (make_annot varP indr)
@@ -553,7 +553,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(my_it_mkProd_or_LetIn
(if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
(mkNamedLambda (make_annot varHC indr) applied_PC'
- (mkVar varHC))|])))))
+ (mkVar varHC))|]))))))
in c, UState.of_context_set ctx
(**********************************************************************)
@@ -620,7 +620,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
(if dep then realsign_ind else realsign)) s)
(mkNamedLambda (make_annot varHC indr) (lift 1 applied_PG)
(mkApp
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+3) realsign_ind)
(mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
@@ -629,7 +629,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
[|mkLambda
(make_annot (Name varHC) indr,
lift (nrealargs+3) applied_PC,
- mkRel 1)|]),
+ mkRel 1)|])),
[|mkVar varHC|]))))))
in c, UState.of_context_set ctx
@@ -825,7 +825,7 @@ let build_congr env (eq,refl,ctx) ind =
(mkIndU indu,
Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
Context.Rel.to_extended_list mkRel 0 realsign))
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (mip.mind_nrealargs+3) realsign)
(mkLambda
@@ -843,7 +843,7 @@ let build_congr env (eq,refl,ctx) ind =
mkVar varH,
[|mkApp (refl,
[|mkVar varB;
- mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+ mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
in c, UState.of_context_set ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcdd23a9c1..633b9da053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+ let clenv = Clenv.update_clenv_evd eqclause evd' in
+ Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
index 1f6b04c1d3..a9100efddb 100644
--- a/tactics/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -35,13 +35,13 @@ type 'a glob_red_flag = {
(** Generic kinds of reductions *)
-type ('a,'b,'c) red_expr_gen =
+type ('a, 'b, 'c, 'flags) red_expr_gen0 =
| Red of bool
| Hnf
- | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
- | Cbv of 'b glob_red_flag
- | Cbn of 'b glob_red_flag
- | Lazy of 'b glob_red_flag
+ | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option
+ | Cbv of 'flags
+ | Cbn of 'flags
+ | Lazy of 'flags
| Unfold of 'b Locus.with_occurrences list
| Fold of 'a list
| Pattern of 'a Locus.with_occurrences list
@@ -49,6 +49,9 @@ type ('a,'b,'c) red_expr_gen =
| CbvVm of ('b,'c) Util.union Locus.with_occurrences option
| CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+type ('a, 'b, 'c) red_expr_gen =
+ ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0
+
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a,'b,'c) red_expr_gen * 'a
@@ -73,7 +76,7 @@ type 'a and_short_name = 'a * Names.lident option
let wit_red_expr :
((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
- (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
- (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
+ (Genintern.glob_constr_and_expr,Tacred.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
+ (EConstr.t,Tacred.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
Genarg.genarg_type =
make0 "redexpr"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..0cc8becd8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -46,7 +46,7 @@ let rec head_bound sigma t = match EConstr.kind sigma t with
| Prod (_, _, b) -> head_bound sigma b
| LetIn (_, _, _, b) -> head_bound sigma b
| App (c, _) -> head_bound sigma c
-| Case (_, _, _, c, _) -> head_bound sigma c
+| Case (_, _, _, _, _, c, _) -> head_bound sigma c
| Ind (ind, _) -> GlobRef.IndRef ind
| Const (c, _) -> GlobRef.ConstRef c
| Construct (c, _) -> GlobRef.ConstructRef c
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
let mk_clenv (c, cty, ctx) =
let sigma = merge_context_set_opt sigma ctx in
let cl = mk_clenv_from_env env sigma None (c,cty) in
- let cl = {cl with templval =
- { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
- env = empty_env}
- in
+ let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+ let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
{ hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
in
let code = match p.code.obj with
@@ -593,7 +591,7 @@ struct
let head_evar sigma c =
let rec hrec c = match EConstr.kind sigma c with
| Evar (evk,_) -> evk
- | Case (_,_,_,c,_) -> hrec c
+ | Case (_,_,_,_,_,c,_) -> hrec c
| App (c,_) -> hrec c
| Cast (c,_,_) -> hrec c
| Proj (p, c) -> hrec c
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(* Only metas are mentioning the old universes. *)
- {
- templval = Evd.map_fl emap clenv.templval;
- templtyp = Evd.map_fl emap clenv.templtyp;
- evd = Evd.map_metas emap evd;
- env = Proofview.Goal.env gl;
- }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ (Evd.map_metas emap evd)
+ (Evd.map_fl emap clenv.templval)
+ (Evd.map_fl emap clenv.templtyp)
| None ->
- { clenv with evd = evd ; env = Proofview.Goal.env gl }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ evd
+ clenv.templval
+ clenv.templtyp
let fresh_hint env sigma h =
let { hint_term = c; hint_uctx = ctx } = h in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 54f4716652..f5947bb946 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -36,7 +36,7 @@ type 'a hint_ast =
| ERes_pf of 'a (* Hint EApply *)
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
- | Unfold_nth of evaluable_global_reference (* Hint Unfold *)
+ | Unfold_nth of Tacred.evaluable_global_reference (* Hint Unfold *)
| Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
type hint = private {
@@ -173,8 +173,8 @@ type hints_entry =
| HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
- | HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
+ | HintsUnfoldEntry of Tacred.evaluable_global_reference list
+ | HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool
| HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index a8747e0a7c..b415b30de8 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -81,7 +81,7 @@ let subst_strategy (subs,(local,obj)) =
local,
List.Smart.map
(fun (k,ql as entry) ->
- let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
+ let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in
if ql==ql' then entry else (k,ql'))
obj
@@ -129,6 +129,9 @@ let set_strategy local str =
type red_expr =
(constr, evaluable_global_reference, constr_pattern) red_expr_gen
+type red_expr_val =
+ (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0
+
let make_flag_constant = function
| EvalVarRef id -> fVAR id
| EvalConstRef sp -> fCONST sp
@@ -221,38 +224,117 @@ let warn_simpl_unfolding_modifiers =
(fun () ->
Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
-let reduction_of_red_expr env =
- let make_flag = make_flag env in
- let rec reduction_of_red_expr = function
+let rec eval_red_expr env = function
+| Simpl (f, o) ->
+ let () =
+ if not (simplIsCbn () || List.is_empty f.rConst) then
+ warn_simpl_unfolding_modifiers () in
+ let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in
+ Simpl (f, o)
+| Cbv f -> Cbv (make_flag env f)
+| Cbn f -> Cbn (make_flag env f)
+| Lazy f -> Lazy (make_flag env f)
+| ExtraRedExpr s ->
+ begin match String.Map.find s !red_expr_tab with
+ | e -> eval_red_expr env e
+ | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *)
+ end
+| (Red _ | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e
+
+let reduction_of_red_expr_val = function
| Red internal ->
if internal then (e_red try_red_product,DEFAULTcast)
else (e_red red_product,DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl (f,o) ->
- let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in
- let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in
- let () =
- if not (simplIsCbn () || List.is_empty f.rConst) then
- warn_simpl_unfolding_modifiers () in
+ let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
+ let am = if simplIsCbn () then strong_cbn f else simpl in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
- | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
+ | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
| Cbn f ->
- (e_red (strong_cbn (make_flag f)), DEFAULTcast)
- | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+ (e_red (strong_cbn f), DEFAULTcast)
+ | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
| Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
| Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
| Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
| ExtraRedExpr s ->
(try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
with Not_found ->
- (try reduction_of_red_expr (String.Map.find s !red_expr_tab)
- with Not_found ->
user_err ~hdr:"Redexpr.reduction_of_red_expr"
- (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
+ (str "unknown user-defined reduction \"" ++ str s ++ str "\""))
| CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
| CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
+
+let reduction_of_red_expr env r =
+ reduction_of_red_expr_val (eval_red_expr env r)
+
+(* Possibly equip a reduction with the occurrences mentioned in an
+ occurrence clause *)
+
+let error_illegal_clause () =
+ CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
+
+let error_illegal_non_atomic_clause () =
+ CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
+
+let error_occurrences_not_unsupported () =
+ CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.")
+
+let bind_red_expr_occurrences occs nbcl redexp =
+ let open Locus in
+ let has_at_clause = function
+ | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
+ | _ -> false in
+ if occs == AllOccurrences then
+ if nbcl > 1 && has_at_clause redexp then
+ error_illegal_non_atomic_clause ()
+ else
+ redexp
+ else
+ match redexp with
+ | Unfold (_::_::_) ->
+ error_illegal_clause ()
+ | Unfold [(occl,c)] ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Unfold [(occs,c)]
+ | Pattern (_::_::_) ->
+ error_illegal_clause ()
+ | Pattern [(occl,c)] ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Pattern [(occs,c)]
+ | Simpl (f,Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Simpl (f,Some (occs,c))
+ | CbvVm (Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ CbvVm (Some (occs,c))
+ | CbvNative (Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ CbvNative (Some (occs,c))
+ | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
+ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
+ error_occurrences_not_unsupported ()
+ | Unfold [] | Pattern [] ->
+ assert false
+
+let reduction_of_red_expr_val ?occs r =
+ let r = match occs with
+ | None -> r
+ | Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r
in
- reduction_of_red_expr
+ reduction_of_red_expr_val r
let subst_mps subst c =
EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
@@ -262,7 +344,7 @@ let subst_red_expr subs =
let sigma = Evd.from_env env in
Redops.map_red_expr_gen
(subst_mps subs)
- (Mod_subst.subst_evaluable_reference subs)
+ (Tacred.subst_evaluable_reference subs)
(Patternops.subst_pattern env sigma subs)
let inReduction : bool * string * red_expr -> obj =
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
index d43785218f..fb0043db8d 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -10,7 +10,6 @@
(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
-open Names
open Constr
open EConstr
open Pattern
@@ -19,10 +18,18 @@ open Reductionops
open Locus
type red_expr =
- (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+ (constr, Tacred.evaluable_global_reference, constr_pattern) red_expr_gen
+
+type red_expr_val
val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
+val eval_red_expr : Environ.env -> red_expr -> red_expr_val
+
+val reduction_of_red_expr_val : ?occs:(Locus.occurrences_expr * int) ->
+ red_expr_val -> e_reduction_function * cast_kind
+
+(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *)
val reduction_of_red_expr :
Environ.env -> red_expr -> e_reduction_function * cast_kind
@@ -42,7 +49,7 @@ val declare_red_expr : bool -> string -> red_expr -> unit
true, the effect is non-synchronous (i.e. it does not survive
section and module closure). *)
val set_strategy :
- bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
+ bool -> (Conv_oracle.level * Tacred.evaluable_global_reference list) list -> unit
(** call by value normalisation function using the virtual machine *)
val cbv_vm : reduction_function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5aa31092e9..b40bdbc25e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -85,24 +85,6 @@ let () =
optread = (fun () -> !universal_lemma_under_conjunctions) ;
optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
-(* The following boolean governs what "intros []" do on examples such
- as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
- if false, it behaves as "intro H; case H; clear H" for fresh H.
- Kept as false for compatibility.
- *)
-
-let bracketing_last_or_and_intro_pattern = ref true
-
-let use_bracketing_last_or_and_intro_pattern () =
- !bracketing_last_or_and_intro_pattern
-
-let () =
- declare_bool_option
- { optdepr = true;
- optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
- optread = (fun () -> !bracketing_last_or_and_intro_pattern);
- optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
-
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -634,70 +616,10 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma dec
in
(sigma, LocalDef (id,b',ty'))
-(* Possibly equip a reduction with the occurrences mentioned in an
- occurrence clause *)
-
-let error_illegal_clause () =
- error "\"at\" clause not supported in presence of an occurrence clause."
-
-let error_illegal_non_atomic_clause () =
- error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
-
-let error_occurrences_not_unsupported () =
- error "Occurrences not supported for this reduction tactic."
-
let bind_change_occurrences occs = function
| None -> None
| Some c -> Some (Redexpr.out_with_occurrences (occs,c))
-let bind_red_expr_occurrences occs nbcl redexp =
- let has_at_clause = function
- | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
- | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
- | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
- | _ -> false in
- if occs == AllOccurrences then
- if nbcl > 1 && has_at_clause redexp then
- error_illegal_non_atomic_clause ()
- else
- redexp
- else
- match redexp with
- | Unfold (_::_::_) ->
- error_illegal_clause ()
- | Unfold [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Unfold [(occs,c)]
- | Pattern (_::_::_) ->
- error_illegal_clause ()
- | Pattern [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Pattern [(occs,c)]
- | Simpl (f,Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Simpl (f,Some (occs,c))
- | CbvVm (Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- CbvVm (Some (occs,c))
- | CbvNative (Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- CbvNative (Some (occs,c))
- | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
- | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
- error_occurrences_not_unsupported ()
- | Unfold [] | Pattern [] ->
- assert false
-
(* The following two tactics apply an arbitrary
reduction function either to the conclusion or to a
certain hypothesis *)
@@ -959,17 +881,16 @@ let reduce redexp cl =
| Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv
| ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*)
in
+ let redexp = Redexpr.eval_red_expr env redexp in
begin match cl.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
| occs ->
- let redexp = bind_red_expr_occurrences occs nbcl redexp in
- let redfun = Redexpr.reduction_of_red_expr env redexp in
+ let redfun = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
e_change_in_concl ~check (revert_cast redfun)
end
<*>
let f (id, occs, where) =
- let redexp = bind_red_expr_occurrences occs nbcl redexp in
- let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+ let (redfun, _) = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
let redfun _ env sigma c = redfun env sigma c in
let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
(id, redfun)
@@ -1083,10 +1004,10 @@ let intros_using_then l tac = intros_using_then_helper tac [] l
let intros = Tacticals.New.tclREPEAT intro
-let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
+let intro_forthcoming_then_gen name_flag move_flag dep_flag bound n tac =
let rec aux n ids =
(* Note: we always use the bound when there is one for "*" and "**" *)
- if (match bound with None -> true | Some (_,p) -> n < p) then
+ if (match bound with None -> true | Some p -> n < p) then
Proofview.tclORELSE
begin
intro_then_gen name_flag move_flag false dep_flag
@@ -1380,20 +1301,18 @@ let do_replace id = function
let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
- let clenv =
- { clenv with evd = Typeclasses.resolve_typeclasses
- ~fail:(not with_evars) clenv.env clenv.evd }
- in
+ let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
+ let clenv = Clenv.update_clenv_evd clenv evd in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
- if not with_evars && occur_meta clenv.evd new_hyp_typ then
+ if not with_evars && occur_meta evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
+ (Proofview.Unsafe.tclEVARS (clear_metas evd))
(Tacticals.New.tclTHENLAST
(assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)
@@ -2306,7 +2225,7 @@ let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
let (forward_subst_one, subst_one) = Hook.make ()
let error_unexpected_extra_pattern loc bound pat =
- let _,nb = Option.get bound in
+ let nb = Option.get bound in
let s1,s2,s3 = match pat with
| IntroNaming (IntroIdentifier _) ->
"name", (String.plural nb " introduction pattern"), "no"
@@ -2339,14 +2258,14 @@ let intro_decomp_eq ?loc l thin tac id =
match my_find_eq_data_decompose env sigma t with
| Some (eq,u,eq_args) ->
!intro_decomp_eq_function
- (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
+ (fun n -> tac ((CAst.make id)::thin) (Some n) l)
(eq,t,eq_args) (c, t)
| None ->
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info (str "Not a primitive equality here.")
end
-let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
+let intro_or_and_pattern ?loc with_evars ll thin tac id =
Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
let env = Proofview.Goal.env gl in
@@ -2360,11 +2279,11 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHENLASTn
(Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
- (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
+ (Array.map2 (fun n l -> tac thin (Some n) l)
nv_with_let ll))
end
-let rewrite_hyp_then assert_style with_evars thin l2r id tac =
+let rewrite_hyp_then with_evars thin l2r id tac =
let rew_on l2r =
Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in
let subst_on l2r x rhs =
@@ -2476,11 +2395,11 @@ let make_tmp_naming avoid l = function
let fit_bound n = function
| None -> true
- | Some (use_bound,n') -> not use_bound || n = n'
+ | Some n' -> n = n'
let exceed_bound n = function
| None -> false
- | Some (use_bound,n') -> use_bound && n >= n'
+ | Some n' -> n >= n'
(* We delay thinning until the completion of the whole intros tactic
to ensure that dependent hypotheses are cleared in the right
@@ -2501,60 +2420,59 @@ let exceed_bound n = function
[patl]: introduction patterns to interpret
*)
-let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
+let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac =
function
| [] when fit_bound n bound ->
tac ids thin
| [] ->
(* Behave as IntroAnonymous *)
- intro_patterns_core with_evars b avoid ids thin destopt bound n tac
+ intro_patterns_core with_evars avoid ids thin destopt bound n tac
[CAst.make @@ IntroNaming IntroAnonymous]
| {CAst.loc;v=pat} :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
match pat with
| IntroForthcoming onlydeps ->
intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt onlydeps n bound
- (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
+ destopt onlydeps bound n
+ (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound
(n+List.length ids) tac l)
| IntroAction pat ->
intro_then_gen (make_tmp_naming avoid l pat)
destopt true false
- (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false
- pat thin destopt
- (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
+ (intro_pattern_action ?loc with_evars pat thin destopt
+ (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0
(fun ids thin ->
- intro_patterns_core with_evars b avoid ids thin destopt bound (n+1) tac l)))
+ intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l)))
| IntroNaming pat ->
- intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound (n+1) tac l
+ intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l
(* Pi-introduction rule, used backwards *)
-and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac l =
+and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l =
match pat with
| IntroIdentifier id ->
check_thin_clash_then id thin avoid (fun thin ->
intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)))
destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)
-and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
+and intro_pattern_action ?loc with_evars pat thin destopt tac id =
match pat with
| IntroWildcard ->
tac (CAst.(make ?loc id)::thin) None []
| IntroOrAndPattern ll ->
- intro_or_and_pattern ?loc with_evars b ll thin tac id
+ intro_or_and_pattern ?loc with_evars ll thin tac id
| IntroInjection l' ->
intro_decomp_eq ?loc l' thin tac id
| IntroRewrite l2r ->
- rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
+ rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None [])
| IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) ->
let naming,tac_ipat =
prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
@@ -2575,28 +2493,26 @@ and prepare_intros ?loc with_evars dft destopt = function
| IntroAction ipat ->
prepare_naming ?loc dft,
(let tac thin bound =
- intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0
+ intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
fun id ->
- intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
+ intro_pattern_action ?loc with_evars ipat [] destopt tac id)
| IntroForthcoming _ -> user_err ?loc
(str "Introduction pattern for one hypothesis expected.")
-let intro_patterns_head_core with_evars b destopt bound pat =
+let intro_patterns_head_core with_evars destopt bound pat =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
check_name_unicity env [] [] pat;
- intro_patterns_core with_evars b Id.Set.empty [] [] destopt
+ intro_patterns_core with_evars Id.Set.empty [] [] destopt
bound 0 (fun _ l -> clear_wildcards l) pat
end
let intro_patterns_bound_to with_evars n destopt =
- intro_patterns_head_core with_evars true destopt
- (Some (true,n))
+ intro_patterns_head_core with_evars destopt (Some n)
let intro_patterns_to with_evars destopt =
- intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
- destopt None
+ intro_patterns_head_core with_evars destopt None
let intro_pattern_to with_evars destopt pat =
intro_patterns_to with_evars destopt [CAst.make pat]
@@ -3271,7 +3187,7 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
(intros_move newlstatus)
let dest_intro_patterns with_evars avoid thin dest pat tac =
- intro_patterns_core with_evars true avoid [] thin dest None 0 tac pat
+ intro_patterns_core with_evars avoid [] thin dest None 0 tac pat
let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
Proofview.tclORELSE
@@ -3377,7 +3293,7 @@ let expand_projections env sigma c =
let rec aux env c =
match EConstr.kind sigma c with
| Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
- | _ -> map_constr_with_full_binders sigma push_rel aux env c
+ | _ -> map_constr_with_full_binders env sigma push_rel aux env c
in
aux env c
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0fd2f1253f..a6471be549 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -179,11 +179,11 @@ val normalise_in_hyp : hyp_location -> unit Proofview.tactic
val normalise_option : goal_location -> unit Proofview.tactic
val normalise_vm_in_concl : unit Proofview.tactic
val unfold_in_concl :
- (occurrences * evaluable_global_reference) list -> unit Proofview.tactic
+ (occurrences * Tacred.evaluable_global_reference) list -> unit Proofview.tactic
val unfold_in_hyp :
- (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic
+ (occurrences * Tacred.evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic
val unfold_option :
- (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
+ (occurrences * Tacred.evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
val change :
check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
val pattern_option :
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index df07dcbca7..f12d4e5de5 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -335,8 +335,9 @@ struct
meta
in
Meta meta
- | Case (ci,c1,_iv,c2,ca) ->
- Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
+ | Case (ci,u1,pms1,c1,_iv,c2,ca) ->
+ let f_ctx (_, p) = pat_of_constr p in
+ Term(DCase(ci,f_ctx c1,pat_of_constr c2,Array.map f_ctx ca))
| Fix ((ia,i),(_,ta,ca)) ->
Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
| CoFix (i,(_,ta,ca)) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:58:25 +0000