summaryrefslogtreecommitdiff
path: root/tactics/extratactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/extratactics.ml4')
-rw-r--r--tactics/extratactics.ml4367
1 files changed, 285 insertions, 82 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ee01f839..0bb6ce96 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: extratactics.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id$ *)
open Pp
open Pcoq
@@ -19,29 +19,45 @@ open Names
open Tacexpr
open Rawterm
open Tactics
-
-(* Equality *)
+open Util
+open Termops
+open Evd
open Equality
+(**********************************************************************)
+(* replace, discriminate, injection, simplify_eq *)
+(* cutrewrite, dependent rewrite *)
+
+let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac =
+ Refiner.tclWITHHOLES false
+ (replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp))
+ sigma1
+ (Option.map Tacinterp.eval_tactic tac)
+
+let replace_multi_term dir_opt (sigma,c) in_hyp =
+ Refiner.tclWITHHOLES false
+ (replace_multi_term dir_opt c)
+ sigma
+ (glob_in_arg_hyp_to_clause in_hyp)
-TACTIC EXTEND replace
- ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ]
+TACTIC EXTEND replace
+ ["replace" open_constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
+-> [ replace_in_clause_maybe_by c1 c2 in_hyp tac ]
END
TACTIC EXTEND replace_term_left
- [ "replace" "->" constr(c) in_arg_hyp(in_hyp) ]
- -> [ replace_multi_term (Some true) c (glob_in_arg_hyp_to_clause in_hyp)]
+ [ "replace" "->" open_constr(c) in_arg_hyp(in_hyp) ]
+ -> [ replace_multi_term (Some true) c in_hyp]
END
TACTIC EXTEND replace_term_right
- [ "replace" "<-" constr(c) in_arg_hyp(in_hyp) ]
- -> [replace_multi_term (Some false) c (glob_in_arg_hyp_to_clause in_hyp)]
+ [ "replace" "<-" open_constr(c) in_arg_hyp(in_hyp) ]
+ -> [replace_multi_term (Some false) c in_hyp]
END
TACTIC EXTEND replace_term
- [ "replace" constr(c) in_arg_hyp(in_hyp) ]
- -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
+ [ "replace" open_constr(c) in_arg_hyp(in_hyp) ]
+ -> [ replace_multi_term None c in_hyp ]
END
let induction_arg_of_quantified_hyp = function
@@ -52,9 +68,13 @@ let induction_arg_of_quantified_hyp = function
ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
ElimOnIdent and not as "constr" *)
+let elimOnConstrWithHoles tac with_evars c =
+ Refiner.tclWITHHOLES with_evars (tac with_evars)
+ c.sigma (Some (ElimOnConstr c.it))
+
TACTIC EXTEND simplify_eq_main
| [ "simplify_eq" constr_with_bindings(c) ] ->
- [ dEq false (Some (ElimOnConstr c)) ]
+ [ elimOnConstrWithHoles dEq false c ]
END
TACTIC EXTEND simplify_eq
[ "simplify_eq" ] -> [ dEq false None ]
@@ -63,7 +83,7 @@ TACTIC EXTEND simplify_eq
END
TACTIC EXTEND esimplify_eq_main
| [ "esimplify_eq" constr_with_bindings(c) ] ->
- [ dEq true (Some (ElimOnConstr c)) ]
+ [ elimOnConstrWithHoles dEq true c ]
END
TACTIC EXTEND esimplify_eq
| [ "esimplify_eq" ] -> [ dEq true None ]
@@ -73,7 +93,7 @@ END
TACTIC EXTEND discriminate_main
| [ "discriminate" constr_with_bindings(c) ] ->
- [ discr_tac false (Some (ElimOnConstr c)) ]
+ [ elimOnConstrWithHoles discr_tac false c ]
END
TACTIC EXTEND discriminate
| [ "discriminate" ] -> [ discr_tac false None ]
@@ -82,7 +102,7 @@ TACTIC EXTEND discriminate
END
TACTIC EXTEND ediscriminate_main
| [ "ediscriminate" constr_with_bindings(c) ] ->
- [ discr_tac true (Some (ElimOnConstr c)) ]
+ [ elimOnConstrWithHoles discr_tac true c ]
END
TACTIC EXTEND ediscriminate
| [ "ediscriminate" ] -> [ discr_tac true None ]
@@ -90,39 +110,40 @@ TACTIC EXTEND ediscriminate
[ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
END
-let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings)
+let h_discrHyp id gl =
+ h_discriminate_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
TACTIC EXTEND injection_main
| [ "injection" constr_with_bindings(c) ] ->
- [ injClause [] false (Some (ElimOnConstr c)) ]
-END
+ [ elimOnConstrWithHoles (injClause []) false c ]
+END
TACTIC EXTEND injection
| [ "injection" ] -> [ injClause [] false None ]
-| [ "injection" quantified_hypothesis(h) ] ->
+| [ "injection" quantified_hypothesis(h) ] ->
[ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
END
TACTIC EXTEND einjection_main
| [ "einjection" constr_with_bindings(c) ] ->
- [ injClause [] true (Some (ElimOnConstr c)) ]
+ [ elimOnConstrWithHoles (injClause []) true c ]
END
TACTIC EXTEND einjection
| [ "einjection" ] -> [ injClause [] true None ]
| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
-END
+END
TACTIC EXTEND injection_as_main
| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
- [ injClause ipat false (Some (ElimOnConstr c)) ]
-END
+ [ elimOnConstrWithHoles (injClause ipat) false c ]
+END
TACTIC EXTEND injection_as
| [ "injection" "as" simple_intropattern_list(ipat)] ->
[ injClause ipat false None ]
| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
[ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
-END
+END
TACTIC EXTEND einjection_as_main
| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
- [ injClause ipat true (Some (ElimOnConstr c)) ]
-END
+ [ elimOnConstrWithHoles (injClause ipat) true c ]
+END
TACTIC EXTEND einjection_as
| [ "einjection" "as" simple_intropattern_list(ipat)] ->
[ injClause ipat true None ]
@@ -130,15 +151,8 @@ TACTIC EXTEND einjection_as
[ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
END
-let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
-
-TACTIC EXTEND conditional_rewrite
-| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
- -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ]
-| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
- "in" hyp(h) ]
- -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ]
-END
+let h_injHyp id gl =
+ h_injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl
TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -152,50 +166,82 @@ TACTIC EXTEND cut_rewrite
-> [ cutRewriteInHyp b eqn id ]
END
-(* Contradiction *)
+(**********************************************************************)
+(* Contradiction *)
+
open Contradiction
TACTIC EXTEND absurd
[ "absurd" constr(c) ] -> [ absurd c ]
END
+let onSomeWithHoles tac = function
+ | None -> tac None
+ | Some c -> Refiner.tclWITHHOLES false tac c.sigma (Some c.it)
+
TACTIC EXTEND contradiction
- [ "contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ]
+ [ "contradiction" constr_with_bindings_opt(c) ] ->
+ [ onSomeWithHoles contradiction c ]
END
-(* AutoRewrite *)
+(**********************************************************************)
+(* AutoRewrite *)
open Autorewrite
-(* J.F : old version
-TACTIC EXTEND autorewrite
- [ "autorewrite" "with" ne_preident_list(l) ] ->
- [ autorewrite Refiner.tclIDTAC l ]
-| [ "autorewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
- [ autorewrite (snd t) l ]
-| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) ] ->
- [ autorewrite_in id Refiner.tclIDTAC l ]
-| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] ->
- [ autorewrite_in id (snd t) l ]
-END
-*)
TACTIC EXTEND autorewrite
| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
[ auto_multi_rewrite l (glob_in_arg_hyp_to_clause cl) ]
| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
- [
- let cl = glob_in_arg_hyp_to_clause cl in
+ [
+ let cl = glob_in_arg_hyp_to_clause cl in
auto_multi_rewrite_with (snd t) l cl
]
END
+TACTIC EXTEND autorewrite_star
+| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
+ [ auto_multi_rewrite ~conds:AllMatches l (glob_in_arg_hyp_to_clause cl) ]
+| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
+ [ let cl = glob_in_arg_hyp_to_clause cl in
+ auto_multi_rewrite_with ~conds:AllMatches (snd t) l cl ]
+END
+
+(**********************************************************************)
+(* Rewrite star *)
+
+let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
+ let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
+ Refiner. tclWITHHOLES false
+ (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings)) sigma true
+
+let occurrences_of = function
+ | n::_ as nl when n < 0 -> (false,List.map abs nl)
+ | nl ->
+ if List.exists (fun n -> n < 0) nl then
+ error "Illegal negative occurrence number.";
+ (true,nl)
+
+TACTIC EXTEND rewrite_star
+| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
+ [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
+ [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] ->
+ [ rewrite_star (Some id) o all_occurrences c tac ]
+| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
+ [ rewrite_star None o (occurrences_of occ) c tac ]
+| [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] ->
+ [ rewrite_star None o all_occurrences c tac ]
+ END
-
+(**********************************************************************)
+(* Hint Rewrite *)
let add_rewrite_hint name ort t lcsr =
let env = Global.env() and sigma = Evd.empty in
- let f c = Constrintern.interp_constr sigma env c, ort, t in
+ let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
add_rew_rules name (List.map f lcsr)
VERNAC COMMAND EXTEND HintRewrite
@@ -204,10 +250,56 @@ VERNAC COMMAND EXTEND HintRewrite
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident(b) ] ->
[ add_rewrite_hint b o t l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+ [ add_rewrite_hint "core" o (Tacexpr.TacId []) l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+ [ add_rewrite_hint "core" o t l ]
END
+(**********************************************************************)
+(* Hint Resolve *)
-(* Refine *)
+open Term
+open Coqlib
+
+let project_hint pri l2r c =
+ let env = Global.env() in
+ let c = Constrintern.interp_constr Evd.empty env c in
+ let t = Retyping.get_type_of env Evd.empty c in
+ let t =
+ Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
+ let sign,ccl = decompose_prod_assum t in
+ let (a,b) = match snd (decompose_app ccl) with
+ | [a;b] -> (a,b)
+ | _ -> assert false in
+ let p =
+ if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+ let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
+ let c = it_mkLambda_or_LetIn
+ (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+ (pri,true,c)
+
+let add_hints_iff l2r lc n bl =
+ Auto.add_hints true bl
+ (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
+
+VERNAC COMMAND EXTEND HintResolveIffLR
+ [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+ ":" preident_list(bl) ] ->
+ [ add_hints_iff true lc n bl ]
+| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+ [ add_hints_iff true lc n ["core"] ]
+END
+VERNAC COMMAND EXTEND HintResolveIffRL
+ [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+ ":" preident_list(bl) ] ->
+ [ add_hints_iff false lc n bl ]
+| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+ [ add_hints_iff false lc n ["core"] ]
+END
+
+(**********************************************************************)
+(* Refine *)
open Refine
@@ -217,7 +309,8 @@ END
let refine_tac = h_refine
-(* Inversion lemmas (Leminv) *)
+(**********************************************************************)
+(* Inversion lemmas (Leminv) *)
open Inv
open Leminv
@@ -263,16 +356,25 @@ VERNAC COMMAND EXTEND DeriveDependentInversionClear
-> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
END
-(* Subst *)
+(**********************************************************************)
+(* Subst *)
TACTIC EXTEND subst
| [ "subst" ne_var_list(l) ] -> [ subst l ]
-| [ "subst" ] -> [ subst_all ]
+| [ "subst" ] -> [ fun gl -> subst_all gl ]
+END
+
+let simple_subst_tactic_flags =
+ { only_leibniz = true; rewrite_dependent_proof = false }
+
+TACTIC EXTEND simple_subst
+| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags ]
END
open Evar_tactics
-(* evar creation *)
+(**********************************************************************)
+(* Evar creation *)
TACTIC EXTEND evar
[ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
@@ -289,7 +391,8 @@ TACTIC EXTEND instantiate
END
-(** Nijmegen "step" tactic for setoid rewriting *)
+(**********************************************************************)
+(** Nijmegen "step" tactic for setoid rewriting *)
open Tactics
open Tactics
@@ -323,40 +426,37 @@ let step left x tac =
(* Main function to push lemmas in persistent environment *)
let cache_transitivity_lemma (_,(left,lem)) =
- if left then
+ if left then
transitivity_left_table := lem :: !transitivity_left_table
else
transitivity_right_table := lem :: !transitivity_right_table
-
-let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_mps subst ref)
+
+let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
let (inTransitivity,_) =
declare_object {(default_object "TRANSITIVITY-STEPS") with
cache_function = cache_transitivity_lemma;
open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
subst_function = subst_transitivity_lemma;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x) }
+ classify_function = (fun o -> Substitute o) }
(* Synchronisation with reset *)
let freeze () = !transitivity_left_table, !transitivity_right_table
-let unfreeze (l,r) =
+let unfreeze (l,r) =
transitivity_left_table := l;
transitivity_right_table := r
-let init () =
+let init () =
transitivity_left_table := [];
transitivity_right_table := []
-let _ =
+let _ =
declare_summary "transitivity-steps"
{ freeze_function = freeze;
unfreeze_function = unfreeze;
- init_function = init;
- survive_module = false;
- survive_section = false }
+ init_function = init }
(* Main entry points *)
@@ -394,10 +494,11 @@ END
-(*spiwack : Vernac commands for retroknowledge *)
+(**********************************************************************)
+(*spiwack : Vernac commands for retroknowledge *)
VERNAC COMMAND EXTEND RetroknowledgeRegister
- | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
+ | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
[ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in
let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in
Global.register f tc tb ]
@@ -405,19 +506,121 @@ END
-(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
+(**********************************************************************)
+(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
defined by Conor McBride *)
TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ]
+| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ]
END
-TACTIC EXTEND generalize_eqs_vars
-| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
+TACTIC EXTEND dep_generalize_eqs
+| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ]
END
+TACTIC EXTEND generalize_eqs_vars
+| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ]
+END
+TACTIC EXTEND dep_generalize_eqs_vars
+| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ]
+END
+
+(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]
+ where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
+ during dependent induction. For internal use. *)
+
+TACTIC EXTEND specialize_eqs
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
+END
+
+(**********************************************************************)
+(* A tactic that considers a given occurrence of [c] in [t] and *)
+(* abstract the minimal set of all the occurrences of [c] so that the *)
+(* abstraction [fun x -> t[x/c]] is well-typed *)
+(* *)
+(* Contributed by Chung-Kil Hur (Winter 2009) *)
+(**********************************************************************)
+
+let subst_var_with_hole occ tid t =
+ let occref = if occ > 0 then ref occ else error_invalid_occurrence [occ] in
+ let locref = ref 0 in
+ let rec substrec = function
+ | RVar (_,id) as x ->
+ if id = tid
+ then (decr occref; if !occref = 0 then x
+ else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+ else x
+ | c -> map_rawconstr_left_to_right substrec c in
+ let t' = substrec t
+ in
+ if !occref > 0 then error_invalid_occurrence [occ] else t'
+
+let subst_hole_with_term occ tc t =
+ let locref = ref 0 in
+ let occref = ref occ in
+ let rec substrec = function
+ | RHole (_,Evd.QuestionMark(Evd.Define true)) ->
+ decr occref; if !occref = 0 then tc
+ else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+ | c -> map_rawconstr_left_to_right substrec c
+ in
+ substrec t
+
+open Tacmach
+
+let out_arg = function
+ | ArgVar _ -> anomaly "Unevaluated or_var variable"
+ | ArgArg x -> x
+
+let hResolve id c occ t gl =
+ let sigma = project gl in
+ let env = clear_named_body id (pf_env gl) in
+ let env_ids = ids_of_context env in
+ let env_names = names_of_rel_context env in
+ let c_raw = Detyping.detype true env_ids env_names c in
+ let t_raw = Detyping.detype true env_ids env_names t in
+ let rec resolve_hole t_hole =
+ try
+ Pretyping.Default.understand sigma env t_hole
+ with
+ | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+ resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+ in
+ let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
+ let t_constr_type = Retyping.get_type_of env sigma t_constr in
+ change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl)) gl
+
+let hResolve_auto id c t gl =
+ let rec resolve_auto n =
+ try
+ hResolve id c n t gl
+ with
+ | UserError _ as e -> raise e
+ | _ -> resolve_auto (n+1)
+ in
+ resolve_auto 1
-TACTIC EXTEND dependent_pattern
-| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ]
+TACTIC EXTEND hresolve_core
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c (out_arg occ) t ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ]
END
-TACTIC EXTEND resolve_classes
-| ["resolve_classes" ] -> [ resolve_classes ]
+(**
+ hget_evar
+*)
+
+open Evar_refiner
+open Sign
+
+let hget_evar n gl =
+ let sigma = project gl in
+ let evl = evar_list sigma (pf_concl gl) in
+ if List.length evl < n then
+ error "Not enough uninstantiated existential variables.";
+ if n <= 0 then error "Incorrect existential variable index.";
+ let ev = List.nth evl (n-1) in
+ let ev_type = existential_type sigma ev in
+ change_in_concl None (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl
+
+TACTIC EXTEND hget_evar
+| [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ]
END
+
+(**********************************************************************)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 21:33:49 +0000