summaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/blast.ml30
-rw-r--r--contrib/interface/depends.ml18
-rw-r--r--contrib/interface/pbp.ml22
-rw-r--r--contrib/interface/showproof.ml4
-rw-r--r--contrib/interface/xlate.ml93
5 files changed, 86 insertions, 81 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 6ec0fac4..767a7dd6 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal =
let d = pf_last_hyp g' in
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
- (add_hint_list hintl local_db) g'))) ::
+ (Hint_db.add_list hintl local_db) g'))) ::
(List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
in
tclFIRST (List.map tclCOMPLETE tacl) goal
and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
- let flags = Auto.auto_unif_flags in
let hintl =
if occur_existential concl then
- list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
- (Hint_db.map_all hdc db)) (local_db::db_list)
+ list_map_append (fun db ->
+ let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+ List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
- (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+ list_map_append (fun db ->
+ let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+ List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
let tac_of_hint =
fun (st, ({pri=b; pat = p; code=t} as _patac)) ->
@@ -279,7 +280,7 @@ module MySearchProblem = struct
let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
in
- let ldb = add_hint_list hintl (List.hd s.localdb) in
+ let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
{ depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
localdb = ldb :: List.tl s.localdb })
@@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl =
tclTHEN intro
(fun g'->
let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
- in trivial_fail_db db_list (add_hint_list hintl local_db) g')
+ in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
in
tclFIRST
(assumption::intro_tac::
@@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl =
(trivial_resolve db_list local_db (pf_concl gl)))) gl
and my_find_search db_list local_db hdc concl =
- let flags = Auto.auto_unif_flags in
let tacl =
if occur_existential concl then
- list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
- (Hint_db.map_all hdc db)) (local_db::db_list)
+ list_map_append (fun db ->
+ let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+ List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
else
- list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
- (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+ list_map_append (fun db ->
+ let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+ List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
in
List.map
(fun (st, {pri=b; pat=p; code=t} as _patac) ->
@@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
with Failure _ -> []
in
(free_try
- (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
+ (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
g'))
in
let rec_tacs =
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index dd40c5cc..203bc9e3 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"
@@ -269,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
igtal
acc)
| TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
- | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+ | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
| TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
| TacArg tacarg -> depends_of_tac_arg tacarg acc
and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
@@ -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 06b957d9..65eadf13 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 953fb5e7..4b9c1332 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 7d1f57fe..da4908e5 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
@@ -684,8 +683,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
@@ -829,11 +828,11 @@ and xlate_tactic =
| [] -> assert false
| fst::others ->
CT_match_tac_rules(fst, others))
- | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
- | TacMatchContext (false,false,rule1::rules) ->
+ | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+ | TacMatchGoal (false,false,rule1::rules) ->
CT_match_context(xlate_context_rule rule1,
List.map xlate_context_rule rules)
- | TacMatchContext (false,true,rule1::rules) ->
+ | TacMatchGoal (false,true,rule1::rules) ->
CT_match_context_reverse(xlate_context_rule rule1,
List.map xlate_context_rule rules)
| TacLetIn (false, l, t) ->
@@ -926,23 +925,26 @@ and xlate_tac =
| TacExtend (_,"contradiction",[]) -> CT_contradiction
| TacDoubleInduction (n1, n2) ->
CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
- | TacExtend (_,"discriminate", [idopt]) ->
+ | TacExtend (_,"discriminate", []) ->
+ CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+ | TacExtend (_,"discriminate", [id]) ->
CT_discriminate_eq
(xlate_quantified_hypothesis_opt
- (out_gen (wit_opt rawwit_quant_hyp) idopt))
- | TacExtend (_,"simplify_eq", [idopt]) ->
- let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
- let idopt2 = match idopt1 with
- None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
- (CT_coerce_NONE_to_ID_OPT CT_none)
- | Some v ->
- CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
- (xlate_quantified_hypothesis v) in
- CT_simplify_eq idopt2
- | TacExtend (_,"injection", [idopt]) ->
+ (Some (out_gen rawwit_quant_hyp id)))
+ | TacExtend (_,"simplify_eq", []) ->
+ CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+ (CT_coerce_NONE_to_ID_OPT CT_none))
+ | TacExtend (_,"simplify_eq", [id]) ->
+ let id1 = out_gen rawwit_quant_hyp id in
+ let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+ (xlate_quantified_hypothesis id1) in
+ CT_simplify_eq id2
+ | TacExtend (_,"injection", []) ->
+ CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+ | TacExtend (_,"injection", [id]) ->
CT_injection_eq
(xlate_quantified_hypothesis_opt
- (out_gen (wit_opt rawwit_quant_hyp) idopt))
+ (Some (out_gen rawwit_quant_hyp id)))
| TacExtend (_,"injection_as", [idopt;ipat]) ->
xlate_error "TODO: injection as"
| TacFix (idopt, n) ->
@@ -967,19 +969,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)
@@ -1150,11 +1155,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)
@@ -1178,10 +1184,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) ->
@@ -1222,19 +1230,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) ->
@@ -1243,13 +1248,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'"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:18:20 +0000