summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/decl_interp.ml4
-rw-r--r--tactics/decl_proof_instr.ml34
-rw-r--r--tactics/decl_proof_instr.mli13
-rw-r--r--tactics/equality.ml23
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/refine.ml8
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--tactics/tactics.ml48
-rw-r--r--tactics/tauto.ml417
11 files changed, 133 insertions, 45 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index c99884c0..62824670 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
open Util
open Names
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
if List.length params <> expected then
errorlabstrm "suppose it is"
(str "Wrong number of extra arguments: " ++
- (if expected = 0 then str "none" else int expected) ++
+ (if expected = 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
let app_ind =
let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 62a8ddfc..67d1d41a 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *)
open Util
open Pp
@@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 =
let clause = build_dep_clause params pat_info per_info hyps gls0 in
let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
let nek =
- register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info
+ register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info
pat_info.pat_pat ek in
let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
tclTHENS (assert_postpone id clause)
@@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id =
let hd2 = applist (mkVar fix_id,args@[obj]) in
compose_lam rc (whd_beta gls.sigma hd2)
+
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
Close_patt t,_ ->
@@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
| Skip_patt (_,t),skipped::next_objs ->
let args0 = push_arg skipped args in
execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
- | End_patt (id,nhyps),[] ->
+ | End_patt (id,(nparams,nhyps)),[] ->
begin
match List.assoc id args with
[None,br_args] ->
- let metas =
- list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+ let all_metas =
+ list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in
+ let param_metas,hyp_metas = list_chop nparams all_metas in
tclTHEN
(tclDO nhrec introf)
(tacnext
- (applist (mkVar id,List.rev_append br_args metas))) gls
+ (applist (mkVar id,
+ List.append param_metas
+ (List.rev_append br_args hyp_metas)))) gls
| _ -> anomaly "wrong stack size"
end
| Split_patt (ids,ind,br), casee::next_objs ->
@@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
| End_patt (_,_) , _ :: _ ->
anomaly "execute_cases : End of branch with garbage left"
-
+let understand_my_constr c gls =
+ let env = pf_env gls in
+ let nc = names_of_rel_context env in
+ let rawc = Detyping.detype false [] nc c in
+ let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in
+ Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+
+let set_refine,my_refine =
+let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in
+((fun tac -> refine:= tac),
+(fun c gls ->
+ let oc = understand_my_constr c gls in
+ !refine oc gls))
(* end focus/claim *)
@@ -1361,7 +1377,7 @@ let end_tac et2 gls =
| ET_Case_analysis,EK_dep tree ->
execute_cases Anonymous pi
(fun c -> tclTHENLIST
- [refine c;
+ [my_refine c;
clear clauses;
justification assumption])
(initial_instance_stack clauses) [pi.per_casee] 0 tree
@@ -1382,7 +1398,7 @@ let end_tac et2 gls =
(fun c ->
tclTHENLIST
[clear [fix_id];
- refine c;
+ my_refine c;
clear clauses;
justification assumption])
(initial_instance_stack clauses)
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 877c8047..5f4a0485 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
open Refiner
open Names
@@ -42,20 +42,20 @@ val execute_cases :
Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
val tree_of_pats :
- identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
split_tree
val add_branch :
- identifier * int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list ->
split_tree -> split_tree
val append_branch :
- identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
(Names.Idset.t * Decl_mode.split_tree) option ->
(Names.Idset.t * Decl_mode.split_tree) option
val append_tree :
- identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list ->
+ identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list ->
split_tree -> split_tree
val build_dep_clause : Term.types Decl_expr.statement list ->
@@ -65,7 +65,7 @@ val build_dep_clause : Term.types Decl_expr.statement list ->
Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
val register_dep_subcase :
- Names.identifier * int ->
+ Names.identifier * (int * int) ->
Environ.env ->
Decl_mode.per_info ->
Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -115,3 +115,4 @@ val init_tree:
(Names.Idset.t * Decl_mode.split_tree) option) ->
Decl_mode.split_tree
+val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58a00419..bf199379 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
+(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *)
open Pp
open Util
@@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) =
else
(cty',rels')
+(* Like the above, but recurse over all the rels found until there are
+ no more rels to be found *)
+let minimal_free_rels_rec env sigma =
+ let rec minimalrec_free_rels_rec prev_rels (c,cty) =
+ let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
+ let combined_rels = Intset.union prev_rels direct_rels in
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+ in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels)))
+ in minimalrec_free_rels_rec Intset.empty
+
(* [sig_clausal_form siglen ty]
Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the
@@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) =
WARNING: No checking is done to make sure that the
sigS(or sigT)'s are actually there.
- - Only homogenious pairs are built i.e. pairs where all the
+ - Only homogeneous pairs are built i.e. pairs where all the
dependencies are of the same sort
[sig_clausal_form] proceed as follows: the default tuple is
@@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
Evd.existential_opt_value (Evd.evars_of !evdref)
(destEvar ev)
with
- | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ | Some w ->
+ let w_type = type_of env sigma w in
+ if Evarconv.e_conv env evdref w_type a then
+ applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ else
+ error "Cannot solve a unification problem."
| None -> anomaly "Not enough components to build the dependent tuple"
in
let scf = sigrec_clausal_form siglen ty in
@@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
*)
let make_iterated_tuple env sigma dflt (z,zty) =
- let (zty,rels) = minimal_free_rels env sigma (z,zty) in
+ let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
let sort_of_zty = get_sort_of env sigma zty in
let sorted_rels = Sort.list (<) (Intset.elements rels) in
let (tuple,tuplety) =
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e517453..4ab40acb 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *)
open Term
open Proof_type
@@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h =
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
-let h_induction_destruct isrec ev l =
+let h_induction_destruct ev isrec l =
abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) ->
List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
- (induction_destruct ev isrec l)
+ (induction_destruct isrec ev l)
let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
@@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l)
(* Constructors *)
let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
(* Moved to tacinterp because of dependencies in Tacinterp.interp
let h_any_constructor t =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 977b602e..af204e77 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *)
open Pp
open Util
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
let rec tclMAP_i n tacfun = function
| [] -> tclDO n (tacfun None)
| a::l ->
- if n=0 then error "Too much names."
+ if n=0 then error "Too many names."
else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
let remember_first_eq id x = if !x = no_move then x := MoveAfter id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e798f59a..4cbfa6c2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
open Pp
open Util
@@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac =
(* ================================= *)
let lemInv id c gls =
+ ignore (pf_get_hyp gls id); (* ensure id exists *)
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (mkVar id) clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
+ | NoSuchBinding ->
+ errorlabstrm ""
+ (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
errorlabstrm "LemInv"
(str "Cannot refine current goal with the lemma " ++
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 322d25e5..ff3f0887 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
@@ -108,6 +108,8 @@ let replace_by_meta env sigma = function
| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
*)
in
+ if occur_meta ty then
+ error "Unable to manage a dependent metavariable of higher-order type.";
mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
exception NoMeta
@@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with
end
| Case (ci,p,cc,v) ->
+ if occur_meta p then
+ error "Unable to manage a metavariable in the return clause of a match.";
(* bof... *)
let nbr = Array.length v in
let v = Array.append [|p;cc|] v in
@@ -380,3 +384,5 @@ let refine (evd,c) gl =
complicated to update meta types when passing through a binder *)
let th = compute_metamap (pf_env gl) evd c in
tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
+
+let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71b50b66..5c891c58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *)
open Constrintern
open Closure
@@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
match_next_pattern find_next')
with
| PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
- match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
+ match_next_pattern (fun () ->
+ let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+ match_pat lmatch hyp pat) ()
| Some patv ->
match b with
| Some body ->
@@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
| PatternMatchingFailure ->
match_next_pattern_in_body next_in_body' () in
match_next_pattern_in_typ
- (fun () -> match_pat lmeta hyp pat) ()
+ (fun () ->
+ let hyp = refresh_universes_strict hyp in
+ match_pat lmeta hyp pat) ()
with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
in
match_next_pattern_in_body
@@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl =
(***************************************************************************)
(* Other entry points *)
-let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+let glob_tactic x =
+ Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
let glob_tactic_env l env x =
Flags.with_option strict_check
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0a8b5d01..0a4c0fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *)
open Pp
open Util
@@ -249,14 +249,51 @@ let change_option occl t = function
Some id -> change_in_hyp occl t id
| None -> change_in_concl occl t
-let change occl c cls =
+let out_arg = function
+ | ArgVar _ -> anomaly "Unevaluated or_var variable"
+ | ArgArg x -> x
+
+let adjust_clause occl cls =
+ (* warn as much as possible on loss of occurrence information *)
(match cls, occl with
({onhyps=(Some(_::_::_)|None)}
|{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
Some _ ->
error "No occurrences expected when changing several hypotheses."
| _ -> ());
- onClauses (change_option occl c) cls
+ (* get at clause from cls if only goal or one hyp specified *)
+ let occl,cls = match occl with
+ | None -> None,cls
+ | Some (occs,c) ->
+ if cls.onhyps=Some[] && occs=all_occurrences then
+ Some (on_snd (List.map out_arg) cls.concl_occs,c),
+ {cls with concl_occs=all_occurrences_expr}
+ else
+ match cls.onhyps with
+ | Some[(occs',id),l] when
+ cls.concl_occs=no_occurrences_expr && occs=all_occurrences ->
+ Some (on_snd (List.map out_arg) occs',c),
+ {cls with onhyps=Some[(all_occurrences_expr,id),l]}
+ | _ ->
+ occl,cls in
+ (* check if cls has still specified occs *)
+ if cls.onhyps <> None &&
+ List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr)
+ (Option.get cls.onhyps)
+ || cls.concl_occs <> all_occurrences_expr &&
+ cls.concl_occs <> no_occurrences_expr
+ then
+ Flags.if_verbose Pp.msg_warning
+ (if cls.onhyps=Some[] then
+ str "Trailing \"at\" modifier not taken into account."
+ else
+ str "\"at\" modifier in clause \"in\" not taken into account.");
+ (* Anticipate on onClauses which removes concl if not at all occs *)
+ if cls.concl_occs=no_occurrences_expr then cls
+ else {cls with concl_occs=all_occurrences_expr}
+
+let change occl c cls =
+ onClauses (change_option occl c) (adjust_clause occl cls)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,DEFAULTcast)
@@ -1397,10 +1434,6 @@ let quantify lconstr =
the left of each x1, ...).
*)
-let out_arg = function
- | ArgVar _ -> anomaly "Unevaluated or_var variable"
- | ArgArg x -> x
-
let occurrences_of_hyp id cls =
let rec hyp_occ = function
[] -> None
@@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl =
let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl =
let env = pf_env gl in
let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+ let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in
let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
let names = compute_induction_names (Array.length indsign) names in
let dephyps = List.map (fun (id,_,_) -> id) deps in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 1729695d..d3e7da6a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*)
open Term
open Hipattern
@@ -20,6 +20,7 @@ open Tacticals
open Tacinterp
open Tactics
open Util
+open Genarg
let assoc_var s ist =
match List.assoc (Names.id_of_string s) ist.lfun with
@@ -97,18 +98,21 @@ let is_conj ist =
let flatten_contravariant_conj ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
+ let hyp = assoc_var "id" ist in
match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+ let hyp = valueIn (VConstr hyp) in
let intros =
iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
<:tactic< idtac >> in
<:tactic<
let newtyp := $newtyp in
- assert newtyp by ($intros; apply id; split; assumption);
- clear id
+ let hyp := $hyp in
+ assert newtyp by ($intros; apply hyp; split; assumption);
+ clear hyp
>>
else
<:tactic<fail>>
@@ -129,16 +133,19 @@ let is_disj ist =
let flatten_contravariant_disj ist =
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
+ let hyp = assoc_var "id" ist in
match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
+ let hyp = valueIn (VConstr hyp) in
iter_tac (list_map_i (fun i arg ->
let typ = valueIn (VConstr (mkArrow arg c)) in
<:tactic<
let typ := $typ in
- assert typ by (intro; apply id; constructor $i; assumption)
- >>) 1 args) <:tactic< clear id >>
+ let hyp := $hyp in
+ assert typ by (intro; apply hyp; constructor $i; assumption)
+ >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
else
<:tactic<fail>>
| _ ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 22:03:22 +0000