aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/functional_principles_proofs.ml10
-rw-r--r--contrib/funind/g_indfun.ml414
-rw-r--r--contrib/funind/indfun.ml2
-rw-r--r--contrib/funind/invfun.ml10
-rw-r--r--contrib/funind/recdef.ml2
-rw-r--r--contrib/interface/depends.ml16
-rw-r--r--contrib/interface/pbp.ml22
-rw-r--r--contrib/interface/showproof.ml4
-rw-r--r--contrib/interface/xlate.ml60
-rw-r--r--contrib/subtac/subtac.ml3
-rw-r--r--contrib/subtac/subtac_obligations.ml1
-rw-r--r--contrib/xml/proofTree2Xml.ml43
12 files changed, 69 insertions, 78 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index d7bcde69c..bd335d304 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
fun g ->
let prov_id = pf_get_new_id hyp_id g in
tclTHENS
- ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+ ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
[tclTHENLIST
[
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
in
(* observe_tac "rec hyp " *)
(tclTHENS
- (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+ (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
[
(* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
(* observe_tac "prove rec hyp" *)
@@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
fun g ->
let prov_hid = pf_get_new_id hid g in
tclTHENLIST[
- forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+ forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
thin [hid];
h_rename [prov_hid,hid]
] g
@@ -1497,7 +1497,7 @@ let prove_principle_for_gen
(tclTHEN
(forward
(Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
- (Genarg.IntroIdentifier wf_thm_id)
+ (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
(mkApp (delayed_force well_founded,[|input_type;relation|])))
(
(* observe_tac *)
@@ -1561,7 +1561,7 @@ let prove_principle_for_gen
);
(* observe_tac "" *) (forward
(Some (prove_rec_arg_acc))
- (Genarg.IntroIdentifier acc_rec_arg_id)
+ (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
(mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
);
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index dae76f2dd..d435f5135 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -90,11 +90,6 @@ END
TACTIC EXTEND newfunind
["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
[
- let pat =
- match pat with
- | None -> IntroAnonymous
- | Some pat -> pat
- in
let c = match cl with
| [] -> assert false
| [c] -> c
@@ -106,11 +101,6 @@ END
TACTIC EXTEND snewfunind
["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
[
- let pat =
- match pat with
- | None -> IntroAnonymous
- | Some pat -> pat
- in
let c = match cl with
| [] -> assert false
| [c] -> c
@@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl =
tclTHEN
(Tactics.letin_tac None (Name idunsafe) cstr allClauses)
(tclTHENFIRST
- (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr))
+ (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr))
Tactics.reflexivity)
gl
@@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
fun gl ->
(functional_induction
true (applist (info.fname, List.rev !list_constr_largs))
- None IntroAnonymous) gl))
+ None None) gl))
nexttac)) ordered_info_list in
(* we try each (f t u v) until one does not fail *)
(* TODO: try also to mix functional schemes *)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a6cbb3211..79ef00972 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -120,7 +120,7 @@ let functional_induction with_clean c princl pat =
princ_infos
args_as_induction_constr
princ'
- pat
+ (None,pat)
None)
subst_and_reduce
g
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 63d44916b..f62d70ab9 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -280,13 +280,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.map
(fun (_,_,br_type) ->
List.map
- (fun id -> Genarg.IntroIdentifier id)
+ (fun id -> dummy_loc, Genarg.IntroIdentifier id)
(generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
)
branches
in
(* before building the full intro pattern for the principle *)
- let pat = Genarg.IntroOrAndPattern intro_pats in
+ let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
let eq_ind = Coqlib.build_coq_eq () in
let eq_construct = mkConstruct((destInd eq_ind),1) in
(* The next to referencies will be used to find out which constructor to apply in each branch *)
@@ -297,7 +297,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
(* We get the identifiers of this branch *)
let this_branche_ids =
List.fold_right
- (fun pat acc ->
+ (fun (_,pat) acc ->
match pat with
| Genarg.IntroIdentifier id -> Idset.add id acc
| _ -> anomaly "Not an identifier"
@@ -447,7 +447,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
[ observe_tac "intro args_names" (tclMAP h_intro args_names);
observe_tac "principle" (forward
(Some (h_exact f_principle))
- (Genarg.IntroIdentifier principle_id)
+ (dummy_loc,Genarg.IntroIdentifier principle_id)
princ_type);
tclTHEN_i
(observe_tac "functional_induction" (
@@ -948,7 +948,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
thin [hid];
h_intro hid;
- Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+ Inv.inv FullInversion None (Rawterm.NamedHyp hid);
(fun g ->
let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 13989f03b..6227f92d7 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -1157,7 +1157,7 @@ let rec introduce_all_values_eq cont_tac functional termine
[] ->
let heq2 = next_global_ident_away true heq_id ids in
tclTHENLIST
- [forward None (IntroIdentifier heq2)
+ [forward None (dummy_loc,IntroIdentifier heq2)
(mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index dd40c5cc3..bf1cf5e7b 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -57,8 +57,7 @@ let explore_tree pfs =
and explain_prim = function
| Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
| Intro identifier -> "Intro"
- | Intro_replacing identifier -> "Intro_replacing"
- | Cut (bool, identifier, types) -> "Cut"
+ | Cut (bool, _, identifier, types) -> "Cut"
| FixRule (identifier, int, l) -> "FixRule"
| Cofix (identifier, l) -> "Cofix"
| Convert_concl (types, cast_kind) -> "Convert_concl"
@@ -281,7 +280,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacExact c
| TacExactNoCheck c
| TacVmCastNoCheck c -> depends_of_'constr c acc
- | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
+ | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
+ | TacApply (_, _, _) -> failwith "TODO"
| TacElim (_, cwb, cwbo) ->
depends_of_'constr_with_bindings cwb
(Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -302,14 +302,13 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
| TacLetTac (_,c,_,_) -> depends_of_'constr c acc
(* Derived basic tactics *)
- | TacSimpleInduction _
- | TacSimpleDestruct _
+ | TacSimpleInductionDestruct _
| TacDoubleInduction _ -> acc
- | TacNewInduction (_, cwbial, cwbo, _, _)
- | TacNewDestruct (_, cwbial, cwbo, _, _) ->
+ | TacInductionDestruct (_, _, [cwbial, cwbo, _, _]) ->
list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
cwbial
(Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+ | TacInductionDestruct (_, _, _) -> failwith "TODO"
| TacDecomposeAnd c
| TacDecomposeOr c -> depends_of_'constr c acc
| TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc)
@@ -410,8 +409,7 @@ let depends_of_compound_rule cr acc = match cr with
and depends_of_prim_rule pr acc = match pr with
| Refine c -> depends_of_constr c acc
| Intro id -> acc
- | Intro_replacing id -> acc
- | Cut (_, _, t) -> depends_of_constr t acc (* TODO: check what 2nd argument contains *)
+ | Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
| FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
| Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
| Convert_concl (t, _) -> depends_of_constr t acc
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 06b957d9c..65eadf13d 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -48,7 +48,7 @@ type pbp_atom =
| PbpTryClear of identifier list
| PbpGeneralize of identifier * identifier list
| PbpLApply of identifier (* = CutAndApply *)
- | PbpIntros of intro_pattern_expr list
+ | PbpIntros of intro_pattern_expr located list
| PbpSplit
(* Existential *)
| PbpExists of identifier
@@ -93,7 +93,7 @@ type pbp_rule = (identifier list *
pbp_sequence option;;
-let make_named_intro id = PbpIntros [IntroIdentifier id];;
+let make_named_intro id = PbpIntros [zz,IntroIdentifier id];;
let make_clears str_list = PbpThen [PbpTryClear str_list]
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
| PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
| PbpIntros l -> TacAtom (zz, TacIntroPattern l)
| PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
- | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
+ | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
| PbpElim (hyp_name, names) ->
let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
TacAtom
@@ -255,9 +255,9 @@ fun avoid c path -> match kind_of_term c, path with
or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
let patt_list =
if a = 1 then
- [cont_patt; IntroIdentifier id2]
+ [zz,cont_patt; zz,IntroIdentifier id2]
else
- [IntroIdentifier id2; cont_patt] in
+ [zz,IntroIdentifier id2; zz,cont_patt] in
(IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank,
total_branches)
| (App(oper, [|c1; c2|]), 2::3::path)
@@ -268,7 +268,7 @@ fun avoid c path -> match kind_of_term c, path with
let id1 = next_global_ident x avoid in
let cont_patt, avoid_names, id, c, path, rank, total_branches =
or_and_tree_to_intro_pattern (id1::avoid) body path in
- (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]],
+ (IntroOrAndPattern[[zz,IntroIdentifier id1; zz,cont_patt]],
avoid_names, id, c, path, rank, total_branches)
| _ -> assert false)
| (App(oper, [|c1; c2|]), 2::a::path)
@@ -282,9 +282,9 @@ fun avoid c path -> match kind_of_term c, path with
let new_rank = if a = 1 then rank else rank+1 in
let patt_list =
if a = 1 then
- [[cont_patt];[IntroIdentifier id2]]
+ [[zz,cont_patt];[zz,IntroIdentifier id2]]
else
- [[IntroIdentifier id2];[cont_patt]] in
+ [[zz,IntroIdentifier id2];[zz,cont_patt]] in
(IntroOrAndPattern patt_list,
avoid_names, id, c, path, new_rank, total_branches+1)
| (_, path) -> let id = next_global_ident hyp_radix avoid in
@@ -305,13 +305,13 @@ let (imply_intro3: pbp_rule) = function
let intro_patt, avoid_names, id, c, p, rank, total_branches =
or_and_tree_to_intro_pattern avoid prem path in
if total_branches = 1 then
- Some(chain_tactics [PbpIntros [intro_patt]]
+ Some(chain_tactics [PbpIntros [zz,intro_patt]]
(f avoid_names clear_names clear_flag (Some id)
(kind_of_term c) path))
else
Some
(PbpThens
- ([PbpIntros [intro_patt]],
+ ([PbpIntros [zz,intro_patt]],
auxiliary_goals clear_names clear_flag id
(rank - 1)
((f avoid_names clear_names clear_flag (Some id)
@@ -667,7 +667,7 @@ let rec cleanup_clears str_list = function
let rec optim3_aux str_list = function
(PbpGeneralize (h,l1))::
- (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others
+ (PbpIntros [zz,IntroIdentifier s])::(PbpGeneralize (h',l2))::others
when s=h' ->
optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
| (PbpTryClear names)::other ->
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 953fb5e79..4b9c1332a 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1197,12 +1197,12 @@ let rec natural_ntree ig ntree =
| TacAssumption -> natural_trivial ig lh g gs ltree
| TacClear _ -> natural_clear ig lh g gs ltree
(* Besoin de l'argument de la tactique *)
- | TacSimpleInduction (NamedHyp id) ->
+ | TacSimpleInductionDestruct (true,NamedHyp id) ->
natural_induction ig lh g gs ge id ltree false
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
natural_induction ig lh g gs ge id ltree true
- | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+ | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
| TacExact c -> natural_exact ig lh g gs (snd c) ltree
| TacCut c -> natural_cut ig lh g gs (snd c) ltree
| TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2e4ff80bb..716f6da3b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -615,8 +615,7 @@ let get_flag r =
(* Rem: EVAR flag obsolète *)
conv_flags, red_ids
-let rec xlate_intro_pattern =
- function
+let rec xlate_intro_pattern (loc,pat) = match pat with
| IntroOrAndPattern [] -> assert false
| IntroOrAndPattern (fp::ll) ->
CT_disj_pattern
@@ -625,7 +624,7 @@ let rec xlate_intro_pattern =
(fun l ->
CT_intro_patt_list(List.map xlate_intro_pattern l))
ll)
- | IntroWildcard _ -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
+ | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
| IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
| IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
| IntroFresh _ -> xlate_error "TODO: IntroFresh"
@@ -686,8 +685,8 @@ let xlate_one_unfold_block = function
;;
let xlate_with_names = function
- IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
- | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+ None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+ | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
@@ -972,19 +971,22 @@ and xlate_tac =
CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
| TacIntrosUntil (AnonHyp n) ->
CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
- | TacIntroMove (Some id1, Some (_,id2)) ->
- CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
- | TacIntroMove (None, Some (_,id2)) ->
- CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2)
- | TacMove (true, id1, id2) ->
+ | TacIntroMove (Some id1, MoveAfter id2) ->
+ CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2)
+ | TacIntroMove (None, MoveAfter id2) ->
+ CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_hyp id2)
+ | TacMove (true, id1, MoveAfter id2) ->
CT_move_after(xlate_hyp id1, xlate_hyp id2)
| TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
+ | TacMove _ -> xlate_error "TODO: move before, at top, at bottom"
| TacIntroPattern patt_list ->
CT_intros
(CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
- | TacIntroMove (Some id, None) ->
+ | TacIntroMove (Some id, MoveToEnd true) ->
CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
- | TacIntroMove (None, None) -> CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+ | TacIntroMove (None, MoveToEnd true) ->
+ CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+ | TacIntroMove _ -> xlate_error "TODO"
| TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
| TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
| TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
@@ -1155,11 +1157,12 @@ and xlate_tac =
xlate_error "TODO: trivial using"
| TacReduce (red, l) ->
CT_reduce (xlate_red_tactic red, xlate_clause l)
- | TacApply (true,false,(c,bindl)) ->
+ | TacApply (true,false,[c,bindl]) ->
CT_apply (xlate_formula c, xlate_bindings bindl)
- | TacApply (true,true,(c,bindl)) ->
+ | TacApply (true,true,[c,bindl]) ->
CT_eapply (xlate_formula c, xlate_bindings bindl)
- | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
+ | TacApply (_,_,_) ->
+ xlate_error "TODO: simple (e)apply and iterated apply"
| TacConstructor (false,n_or_meta, bindl) ->
let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1183,10 +1186,12 @@ and xlate_tac =
| TacCase (false,(c1,sl)) ->
CT_casetac (xlate_formula c1, xlate_bindings sl)
| TacElim (true,_,_) | TacCase (true,_)
- | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
+ | TacInductionDestruct (_,true,_) ->
xlate_error "TODO: eelim, ecase, edestruct, einduction"
- | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
- | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
+ | TacSimpleInductionDestruct (true,h) ->
+ CT_induction (xlate_quantified_hypothesis h)
+ | TacSimpleInductionDestruct (false,h) ->
+ CT_destruct (xlate_quantified_hypothesis h)
| TacCut c -> CT_cut (xlate_formula c)
| TacLApply c -> CT_use (xlate_formula c)
| TacDecompose ([],c) ->
@@ -1227,19 +1232,16 @@ and xlate_tac =
CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
| TacDAuto (a, b, _) ->
xlate_error "TODO: dauto using"
- | TacNewDestruct(false,a,b,c,None) ->
+ | TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
CT_new_destruct
(List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
- | TacNewInduction(false,a,b,c,None) ->
+ | TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
CT_new_induction
(List.map xlate_int_or_constr a, xlate_using b,
xlate_with_names c)
- | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
- | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
- (*| TacInstantiate (a, b, cl) ->
- CT_instantiate(CT_int a, xlate_formula b,
- assert false) *)
+ | TacInductionDestruct(_,false,_) ->
+ xlate_error "TODO: clause 'in' and full 'as' of destruct/induction"
| TacLetTac (na, c, cl, true) when cl = nowhere ->
CT_pose(xlate_id_opt_aux na, xlate_formula c)
| TacLetTac (na, c, cl, true) ->
@@ -1248,13 +1250,13 @@ and xlate_tac =
but the structures are different *)
xlate_clause cl)
| TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
- | TacAssert (None, IntroIdentifier id, c) ->
+ | TacAssert (None, (_,IntroIdentifier id), c) ->
CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (None, IntroAnonymous, c) ->
+ | TacAssert (None, (_,IntroAnonymous), c) ->
CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
- | TacAssert (Some (TacId []), IntroIdentifier id, c) ->
+ | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) ->
CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
- | TacAssert (Some (TacId []), IntroAnonymous, c) ->
+ | TacAssert (Some (TacId []), (_,IntroAnonymous), c) ->
CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
| TacAssert _ ->
xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index c36c6458d..baf565ab1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -231,7 +231,8 @@ let subtac (loc, command) =
debug 2 (Himsg.explain_pretype_error env exn);
raise e
- | (Stdpp.Exc_located (loc, e')) as e ->
+ | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+ Stdpp.Exc_located (loc, e') as e) ->
debug 2 (str "Parsing exception: ");
(match e' with
| Type_errors.TypeError (env, exn) ->
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 4e824921b..a393e2c9b 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac =
true
else false
with
+ | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
| Stdpp.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (obl.obl_location, "solve_obligation", s)
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 9afd07a61..05be01bc6 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,7 @@ let first_word s =
let string_of_prim_rule x = match x with
| Proof_type.Intro _-> "Intro"
- | Proof_type.Intro_replacing _-> "Intro_replacing"
- | Proof_type.Cut (_,_,_) -> "Cut"
+ | Proof_type.Cut _ -> "Cut"
| Proof_type.FixRule (_,_,_) -> "FixRule"
| Proof_type.Cofix (_,_)-> "Cofix"
| Proof_type.Refine _ -> "Refine"
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:21:27 +0000