aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml7
-rw-r--r--tactics/eqschemes.ml6
-rw-r--r--tactics/equality.ml28
-rw-r--r--tactics/hipattern.ml58
-rw-r--r--tactics/ppred.ml1
-rw-r--r--tactics/tacticals.ml14
-rw-r--r--tactics/tactics.ml10
8 files changed, 68 insertions, 58 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f824552705..3b8232d20a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
let try_do_hyps treat_id l =
autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
in
- if cl.concl_occs != AllOccurrences &&
+ if not (Locusops.is_all_occurrences cl.concl_occs) &&
cl.concl_occs != NoOccurrences
then
Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e505bb3a42..a3620f4081 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -230,8 +230,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
let sigma' =
- Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
- cl.cl_concl concl sigma'
+ Evarconv.(unify_leq_delay
+ ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
+ env sigma' cl.cl_concl concl)
in (sigma', term) end
let unify_resolve_refine poly flags gl clenv =
@@ -1111,7 +1112,7 @@ let initial_select_evars filter =
let resolve_typeclass_evars debug depth unique env evd filter split fail =
let evd =
try Evarconv.solve_unif_constraints_with_heuristics
- ~ts:(Typeclasses.classes_transparent_state ()) env evd
+ ~flags:(Evarconv.default_flags_of (Typeclasses.classes_transparent_state ())) env evd
with e when CErrors.noncritical e -> evd
in
resolve_all_evars debug depth unique env
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b12018cd66..3c1115d056 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) =
let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
if List.exists is_local_def realsign then
error "Inductive equalities with local definitions in arity not supported.";
- let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+ let constrsign,ccl = mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments"; (* This can be relaxed... *)
@@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) =
let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
if List.exists is_local_def realsign then
error "Inductive equalities with local definitions in arity not supported";
- let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+ let constrsign,ccl = mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
@@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind =
error "Inductive equalities with local definitions in arity not supported.";
let env_with_arity = push_rel_context arityctxt env in
let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
- let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+ let constrsign,ccl = mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 769e702da1..4a1bb37fa4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
((c,l) : constr with_bindings) with_evars =
- if occs != AllOccurrences then (
+ if not (Locusops.is_all_occurrences occs) then (
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
Proofview.Goal.enter begin fun gl ->
@@ -595,15 +595,16 @@ let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
else check_required_library ["Coq";"Setoids";"Setoid"]
-let check_setoid cl =
+let check_setoid cl =
+ let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in
Option.fold_left
- ( List.fold_left
+ (List.fold_left
(fun b ((occ,_),_) ->
- b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences)
+ b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ)))
)
)
- ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) &&
- (Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences))
+ (not (Locusops.is_all_occurrences concloccs) &&
+ (concloccs <> NoOccurrences))
cl.onhyps
let replace_core clause l2r eq =
@@ -635,7 +636,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
let evd =
if unsafe then Some (Tacmach.New.project gl)
else
- try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
+ try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2)
with Evarconv.UnableToUnify _ -> None
in
match evd with
@@ -1193,9 +1194,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
(* is the default value typable with the expected type *)
let dflt_typ = unsafe_type_of env sigma dflt in
try
- let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
- let sigma =
- Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in
+ let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
sigma, dflt
with Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
@@ -1210,11 +1210,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
match evopt with
| Some w ->
let w_type = unsafe_type_of env sigma w in
- begin match Evarconv.cumul env sigma w_type a with
- | Some sigma ->
+ begin match Evarconv.unify_leq_delay env sigma w_type a with
+ | sigma ->
let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
- | None ->
+ | exception Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
end
| None ->
@@ -1724,7 +1724,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
tclTHENLIST
((if need_rewrite then
[revert (List.map snd dephyps);
- general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
+ general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp);
(tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
else
[Proofview.tclUNIT ()]) @
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 708412720a..395b4928ce 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
&& (Int.equal mip.mind_nrealargs 0)
then
if is_strict_conjunction style (* strict conjunction *) then
- let ctx =
- (prod_assum sigma (snd
- (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in
+ let (ctx, _) = mip.mind_nf_lc.(0) in
+ let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
if
+ (* Constructor has a type of the form
+ c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **)
List.for_all
(fun decl -> let c = RelDecl.get_type decl in
is_local_assum decl &&
- isRel sigma c &&
- Int.equal (destRel sigma c) mib.mind_nparams) ctx
+ Constr.isRel c &&
+ Int.equal (Constr.destRel c) mib.mind_nparams) ctx
then
Some (hdapp,args)
else None
else
+ let ctx, cty = mip.mind_nf_lc.(0) in
+ let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
let ctyp = whd_beta_prod sigma
- (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
- (EConstr.of_constr mip.mind_nf_lc.(0)) args) in
+ (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
(* Record or non strict conjunction *)
@@ -165,12 +167,13 @@ let is_tuple sigma t =
it is strict if it has the form
"Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
-let test_strict_disjunction n lc =
- let open Term in
- Array.for_all_i (fun i c ->
- match (prod_assum (snd (decompose_prod_n_assum n c))) with
- | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
- | _ -> false) 0 lc
+let test_strict_disjunction (mib, mip) =
+ let n = List.length mib.mind_params_ctxt in
+ let check i (ctx, _) = match List.skipn n (List.rev ctx) with
+ | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
+ | _ -> false
+ in
+ Array.for_all_i check 0 mip.mind_nf_lc
let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
let (hdapp,args) = decompose_app sigma t in
@@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
&& (Int.equal mip.mind_nrealargs 0)
then
if strict then
- if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
+ if test_strict_disjunction (mib, mip) then
Some (hdapp,args)
else
None
else
- let cargs =
- Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args)))
- mip.mind_nf_lc in
+ let map (ctx, cty) =
+ let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+ pi2 (destProd sigma (prod_applist sigma ar args))
+ in
+ let cargs = Array.map map mip.mind_nf_lc in
Some (hdapp,Array.to_list cargs)
else
None
@@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t =
match EConstr.kind sigma hdapp with
| Ind (ind , _) ->
let (mib,mip) = Global.lookup_inductive ind in
- let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
- if Int.equal nconstr 1 && zero_args constr_types.(0) then
+ if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
Some hdapp
else
None
@@ -308,11 +311,13 @@ let match_with_equation env sigma t =
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
if Int.equal nconstr 1 then
- if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
+ let (ctx, cty) = constr_types.(0) in
+ let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+ if is_matching env sigma coq_refl_leibniz1_pattern cty then
None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
- else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_leibniz2_pattern cty then
None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
+ else if is_matching env sigma coq_refl_jm_pattern cty then
None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else raise NoEquationFound
else raise NoEquationFound
@@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t =
| Ind (ind, _) ->
let (mib,mip) = Global.lookup_inductive ind in
if Array.length (mib.mind_packets)>1 then None else
- let nodep_constr c =
- has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in
+ let nodep_constr (ctx, cty) =
+ let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+ has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in
if Array.for_all nodep_constr mip.mind_nf_lc then
let params=
if Int.equal mip.mind_nrealargs 0 then args else
@@ -400,7 +406,7 @@ let match_with_sigma_type sigma t =
&& (Int.equal mip.mind_nrealargs 0)
&& (Int.equal (Array.length mip.mind_consnames)1)
&& has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
- (EConstr.of_constr mip.mind_nf_lc.(0))
+ (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx))
then
(*allowing only 1 existential*)
Some (hdapp,args)
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
index dd1bcd4699..d832dc279c 100644
--- a/tactics/ppred.ml
+++ b/tactics/ppred.ml
@@ -6,6 +6,7 @@ open Pputils
let pr_with_occurrences pr keyword (occs,c) =
match occs with
+ | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +")
| AllOccurrences ->
pr c
| NoOccurrences ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bfbce8f6eb..ec8d4d0e14 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -20,6 +20,7 @@ open Tacmach
open Clenv
open Tactypes
+module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(************************************************************************)
@@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true
(* Compute the let-in signature of case analysis or standard induction scheme *)
let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
let rec analrec c recargs =
- match Constr.kind c, recargs with
- | Prod (_,_,c), recarg::rest ->
+ match c, recargs with
+ | RelDecl.LocalAssum _ :: c, recarg::rest ->
let rest = analrec c rest in
begin match Declareops.dest_recarg recarg with
| Norec | Imbr _ -> true :: rest
@@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
if rec_flag && Int.equal j k then true :: true :: rest
else true :: rest
end
- | LetIn (_,_,_,c), rest -> false :: analrec c rest
- | _, [] -> []
+ | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest
+ | [], [] -> []
| _ -> anomaly (Pp.str "compute_constructor_signatures.")
in
let (mib,mip) = Global.lookup_inductive ity in
- let n = mib.mind_nparams in
- let lc =
- Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
+ let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
+ let lc = Array.map map mip.mind_nf_lc in
let lrecargs = Declareops.dest_subterms mip.mind_recargs in
Array.map2 analrec lc lrecargs
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index db59f7cfc2..415225454a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3840,9 +3840,9 @@ let specialize_eqs id =
let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
compare_upto_variables !evars c1 c2 &&
- (match Evarconv.conv env !evars c1 c2 with
- | Some sigma -> evars := sigma; true
- | None -> false)
+ (match Evarconv.unify_delay env !evars c1 c2 with
+ | sigma -> evars := sigma; true
+ | exception Evarconv.UnableToUnify _ -> false)
in
let rec aux in_eqs ctx acc ty =
match EConstr.kind !evars ty with
@@ -4398,7 +4398,9 @@ let check_expected_type env sigma (elimc,bl) elimt =
let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
let sigma = solve_evar_clause env sigma true cl bl in
let (_,u,_) = destProd sigma cl.cl_concl in
- fun t -> Option.has_some (Evarconv.cumul env sigma t u)
+ fun t -> match Evarconv.unify_leq_delay env sigma t u with
+ | _sigma -> true
+ | exception Evarconv.UnableToUnify _ -> false
let check_enough_applied env sigma elim =
(* A heuristic to decide whether the induction arg is enough applied *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:03:46 +0000