aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/firstorder/rules.ml6
-rw-r--r--contrib/funind/functional_principles_proofs.ml13
-rw-r--r--contrib/funind/invfun.ml5
-rw-r--r--contrib/funind/recdef.ml24
-rw-r--r--contrib/interface/blast.ml4
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/interface/showproof.ml4
-rw-r--r--contrib/interface/xlate.ml42
-rw-r--r--contrib/omega/coq_omega.ml2
-rw-r--r--contrib/ring/ring.ml6
-rw-r--r--contrib/setoid_ring/newring.ml43
11 files changed, 63 insertions, 48 deletions
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index b6112e653..813e951cf 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
let defined_connectives=lazy
- [[],EvalConstRef (destConst (constant "not"));
- [],EvalConstRef (destConst (constant "iff"))]
+ [all_occurrences,EvalConstRef (destConst (constant "not"));
+ all_occurrences,EvalConstRef (destConst (constant "iff"))]
let normalize_evaluables=
onAllClauses
@@ -213,4 +213,4 @@ let normalize_evaluables=
None->unfold_in_concl (Lazy.force defined_connectives)
| Some ((_,id),_)->
unfold_in_hyp (Lazy.force defined_connectives)
- (([],id),Tacexpr.InHypTypeOnly))
+ ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly))
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 558ca6c21..3d80bd004 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -637,7 +637,7 @@ let build_proof
[
h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
- pattern_option [[-1],t] None;
+ pattern_option [(false,[1]),t] None;
h_simplest_case t;
(fun g' ->
let g'_nb_prod = nb_prod (pf_concl g') in
@@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [([],Names.EvalConstRef fname)];
+ [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
let do_prove =
build_proof
interactive_proof
@@ -1347,11 +1347,10 @@ let build_clause eqs =
{
Tacexpr.onhyps =
Some (List.map
- (fun id -> ([],id),Tacexpr.InHyp)
+ (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
eqs
);
- Tacexpr.onconcl = false;
- Tacexpr.concl_occs = []
+ Tacexpr.concl_occs = Rawterm.no_occurrences_expr
}
let rec rewrite_eqs_in_eqs eqs =
@@ -1364,7 +1363,7 @@ let rec rewrite_eqs_in_eqs eqs =
(fun id gl ->
observe_tac
(Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
- (tclTRY (Equality.general_rewrite_in true [] id (mkVar eq) false))
+ (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false))
gl
)
eqs
@@ -1386,7 +1385,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
(fun g ->
if is_mes
then
- unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g
+ unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
else tclIDTAC g
);
observe_tac "rew_and_finish"
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index a5bd519e2..0160c290f 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -16,6 +16,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
+open Termops
open Sign
open Hiddentac
@@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
| None -> (id::pre_args,pre_tac)
| Some b ->
(pre_args,
- tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac
+ tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
)
else (pre_args,pre_tac)
@@ -687,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
h_generalize (List.map mkVar ids);
thin ids
]
- else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
+ else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))]
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index f4f852d36..13989f03b 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -296,7 +296,7 @@ let mkCaseEq a : tactic =
[h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
(fun g2 ->
change_in_concl None
- (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2))
+ (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2))
g2);
simplest_case a] g);;
@@ -323,7 +323,7 @@ let mkDestructEq :
[h_generalize new_hyps;
(fun g2 ->
change_in_concl None
- (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+ (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
simplest_case expr], to_revert
let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
@@ -336,7 +336,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
h_intros thin_intros;
tclMAP
- (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false))
+ (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false))
(List.rev eqs);
(fun g1 ->
let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -397,7 +397,7 @@ let tclUSER tac is_mes l g =
clear_tac;
if is_mes
then tclTHEN
- (unfold_in_concl [([], evaluable_of_global_reference
+ (unfold_in_concl [(all_occurrences, evaluable_of_global_reference
(delayed_force ltof_ref))])
tac
else tac
@@ -496,7 +496,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
Nameops.out_name k_na,Nameops.out_name def_na
in
tclTHENS
- (general_rewrite_bindings false []
+ (general_rewrite_bindings false all_occurrences
(mkVar eq,
ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
dummy_loc, NamedHyp def_id, mkVar def]) false)
@@ -531,7 +531,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
observe_tac "intros k h' def" (h_intros [k;h';def]);
observe_tac "simple_iter" (simpl_iter onConcl);
observe_tac "unfold functional"
- (unfold_in_concl[([1],evaluable_of_global_reference func)]);
+ (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]);
observe_tac "rewriting equations"
(list_rewrite true eqs);
observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs);
@@ -1120,7 +1120,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let x = n_x_id ids nargs in
tclTHENLIST [
h_intros x;
- unfold_in_concl [([], evaluable_of_global_reference f)];
+ unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)];
observe_tac "simplest_case"
(simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x))));
@@ -1144,7 +1144,7 @@ let base_leaf_eq func eqs f_id g =
[|mkApp (delayed_force coq_S, [|mkVar p|]);
mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
simpl_iter onConcl;
- tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]);
+ tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]);
list_rewrite true eqs;
apply (delayed_force refl_equal)] g;;
@@ -1160,9 +1160,9 @@ let rec introduce_all_values_eq cont_tac functional termine
[forward None (IntroIdentifier heq2)
(mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
simpl_iter (onHyp heq2);
- unfold_in_hyp [([1], evaluable_of_global_reference
+ unfold_in_hyp [((true,[1]), evaluable_of_global_reference
(global_of_constr functional))]
- (([], heq2), Tacexpr.InHyp);
+ ((all_occurrences_expr, heq2), Tacexpr.InHyp);
tclTHENS
(fun gls ->
let t_eq = compute_renamed_type gls (mkVar heq2) in
@@ -1170,7 +1170,7 @@ let rec introduce_all_values_eq cont_tac functional termine
let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in
Nameops.out_name def_na
in
- observe_tac "rewrite heq" (general_rewrite_bindings false []
+ observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences
(mkVar heq2,
ExplicitBindings[dummy_loc,NamedHyp def_id,
f]) false) gls)
@@ -1226,7 +1226,7 @@ let rec introduce_all_values_eq cont_tac functional termine
f_S(mkVar pmax');
dummy_loc, NamedHyp def_id, f])
in
- observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false []
+ observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences
c_b false))
g
)
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 10fafaefc..6ec0fac42 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -188,7 +188,7 @@ and e_my_find_search db_list local_db hdc concl =
| Res_pf_THEN_trivial_fail (term,cl) ->
tclTHEN (unify_e_resolve (term,cl))
(e_trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_in_concl [[],c]
+ | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
| Extern tacast -> Auto.conclPattern concl
(Option.get p) tacast
in
@@ -403,7 +403,7 @@ and my_find_search db_list local_db hdc concl =
tclTHEN
(unify_resolve st (term,cl))
(trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_in_concl [[],c]
+ | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
| Extern tacast ->
conclPattern concl (Option.get p) tacast))
tacl
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index ac152f906..06b957d9c 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function
TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
| PbpGeneralize (h,args) ->
let l = List.map make_pbp_pattern args in
- TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous])
+ TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous])
| PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
| PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
| PbpIntros l -> TacAtom (zz, TacIntroPattern l)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index a2a504fb4..953fb5e79 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1612,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree =
| _ -> assert false
and natural_reduce ig lh g gs ge mode la ltree =
match la with
- {onhyps=Some[];onconcl=true} ->
+ {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr ->
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
@@ -1620,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree =
{ihsg=All_subgoals_hyp;isgintro="simpl"})
ltree)
]
- | {onhyps=Some[hyp]; onconcl=false} ->
+ | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr ->
spv
[ (natural_lhyp lh ig.ihsg);
(show_goal2 lh ig g gs "");
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b041272c1..fa8f05713 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -464,24 +464,31 @@ let (xlate_ident_or_metaid:
AI (_, x) -> xlate_ident x
| MetaId(_, x) -> CT_metaid x;;
+let nums_of_occs (b,nums) =
+ if b then nums
+ else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums
+
let xlate_hyp = function
| AI (_,id) -> xlate_ident id
| MetaId _ -> xlate_error "MetaId should occur only in quotations"
let xlate_hyp_location =
function
- | (nums, AI (_,id)), InHypTypeOnly ->
- CT_intype(xlate_ident id, nums_or_var_to_int_list nums)
- | (nums, AI (_,id)), InHypValueOnly ->
- CT_invalue(xlate_ident id, nums_or_var_to_int_list nums)
- | ([], AI (_,id)), InHyp ->
+ | (occs, AI (_,id)), InHypTypeOnly ->
+ CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+ | (occs, AI (_,id)), InHypValueOnly ->
+ CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+ | ((true,[]), AI (_,id)), InHyp ->
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_coerce_ID_to_UNFOLD (xlate_ident id))
- | (a::l, AI (_,id)), InHyp ->
+ | ((_,a::l as occs), AI (_,id)), InHyp ->
+ let nums = nums_of_occs occs in
+ let a = List.hd nums and l = List.tl nums in
CT_coerce_UNFOLD_to_HYP_LOCATION
(CT_unfold_occ (xlate_ident id,
CT_int_ne_list(num_or_var_to_int a,
nums_or_var_to_int_list_aux l)))
+ | ((false,[]), AI (_,id)), InHyp -> xlate_error "Unused"
| (_, MetaId _),_ ->
xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
@@ -494,7 +501,7 @@ let xlate_clause cls =
| Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
CT_clause
(hyps_info,
- if cls.onconcl then
+ if cls.concl_occs <> no_occurrences_expr then
CT_coerce_STAR_to_STAR_OPT CT_star
else
CT_coerce_NONE_to_STAR_OPT CT_none)
@@ -667,11 +674,13 @@ let xlate_using = function
| Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
let xlate_one_unfold_block = function
- ([],qid) ->
+ ((true,[]),qid) ->
CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
- | (n::nums, qid) ->
+ | (((_,_::_) as occs), qid) ->
+ let l = nums_of_occs occs in
CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid,
- nums_or_var_to_int_ne_list n nums)
+ nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
+ | ((false,[]), qid) -> xlate_error "Unused"
;;
let xlate_with_names = function
@@ -732,7 +741,8 @@ and xlate_red_tactic =
| CbvVm -> CT_cbvvm
| Hnf -> CT_hnf
| Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
- | Simpl (Some (l,c)) ->
+ | Simpl (Some (occs,c)) ->
+ let l = nums_of_occs occs in
CT_simpl
(CT_coerce_PATTERN_to_PATTERN_OPT
(CT_pattern_occ
@@ -751,9 +761,9 @@ and xlate_red_tactic =
| Fold formula_list ->
CT_fold(CT_formula_list(List.map xlate_formula formula_list))
| Pattern l ->
- let pat_list = List.map (fun (nums,c) ->
+ let pat_list = List.map (fun (occs,c) ->
CT_pattern_occ
- (CT_int_list (nums_or_var_to_int_list_aux nums),
+ (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)),
xlate_formula c)) l in
(match pat_list with
| first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
@@ -907,6 +917,7 @@ and xlate_tac =
| TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
| TacChange (Some(l,c), f, b) ->
(* TODO LATER: combine with other constructions of pattern_occ *)
+ let l = nums_of_occs l in
CT_change_local(
CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l),
xlate_formula c),
@@ -1151,8 +1162,9 @@ and xlate_tac =
| TacSpecialize (nopt, (c,sl)) ->
CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
| TacGeneralize [] -> xlate_error ""
- | TacGeneralize ((([],first),Anonymous) :: cl)
- when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl ->
+ | TacGeneralize ((((true,[]),first),Anonymous) :: cl)
+ when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
+ & na = Anonymous) cl ->
CT_generalize
(CT_formula_ne_list (xlate_formula first,
List.map (fun ((_,c),_) -> xlate_formula c) cl))
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index b96b57d5b..0bb18b3b0 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -133,7 +133,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c
let generalize_tac t = generalize_time (generalize t)
let elim t = elim_time (simplest_elim t)
let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [[], Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
let rev_assoc k =
let rec loop = function
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 66246faf5..92f74d1d9 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -826,9 +826,11 @@ let raw_polynom th op lc gl =
c'''i; ci; c'i_eq_c''i |]))))
(tclTHENS
(tclORELSE
- (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i
+ (Setoid_replace.general_s_rewrite true
+ Termops.all_occurrences c'i_eq_c''i
~new_goals:[])
- (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i
+ (Setoid_replace.general_s_rewrite false
+ Termops.all_occurrences c'i_eq_c''i
~new_goals:[]))
[tac]))
else
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c3caa403e..474b3616a 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -104,7 +104,8 @@ let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));;
+ Tactics.reduct_option (protect_red map,DEFAULTcast)
+ (Some((all_occurrences_expr,id),InHyp));;
TACTIC EXTEND protect_fv
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 06:51:31 +0000