aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-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
4 files changed, 32 insertions, 20 deletions
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))
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 07:13:18 +0000