aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/evar_tactics.ml33
-rw-r--r--ltac/evar_tactics.mli2
-rw-r--r--ltac/extraargs.ml42
-rw-r--r--ltac/extratactics.ml422
-rw-r--r--ltac/rewrite.ml11
-rw-r--r--ltac/tacinterp.ml2
6 files changed, 35 insertions, 37 deletions
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 6b94da28a9..01cff94a8c 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -7,6 +7,9 @@
(************************************************************************)
open Util
+open Names
+open Term
+open EConstr
open CErrors
open Evar_refiner
open Tacmach
@@ -35,25 +38,32 @@ let instantiate_evar evk (ist,rawc) sigma =
let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
tclEVARS sigma'
+let evar_list sigma c =
+ let rec evrec acc c =
+ match EConstr.kind sigma c with
+ | Evar (evk, _ as ev) -> ev :: acc
+ | _ -> EConstr.fold sigma evrec acc c in
+ evrec [] c
+
let instantiate_tac n c ido =
Proofview.V82.tactic begin fun gl ->
let sigma = gl.sigma in
let evl =
match ido with
- ConclLocation () -> evar_list (pf_concl gl)
+ ConclLocation () -> evar_list sigma (pf_concl gl)
| HypLocation (id,hloc) ->
let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
match hloc with
InHyp ->
(match decl with
- | LocalAssum (_,typ) -> evar_list typ
+ | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
| _ -> error
"Please be more specific: in type or value?")
| InHypTypeOnly ->
- evar_list (NamedDecl.get_type decl)
+ evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
| InHypValueOnly ->
(match decl with
- | LocalDef (_,body,_) -> evar_list body
+ | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
| _ -> error "Not a defined hypothesis.") in
if List.length evl < n then
error "Not enough uninstantiated existential variables.";
@@ -92,3 +102,18 @@ let let_evar name typ =
in
Sigma (tac, sigma, p)
end }
+
+let hget_evar n =
+ let open EConstr in
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let sigma = Tacmach.New.project gl in
+ let concl = Proofview.Goal.concl gl in
+ let evl = evar_list sigma concl 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 = EConstr.existential_type sigma ev in
+ Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
+ end }
+
diff --git a/ltac/evar_tactics.mli b/ltac/evar_tactics.mli
index 41266e61c3..cfe7476658 100644
--- a/ltac/evar_tactics.mli
+++ b/ltac/evar_tactics.mli
@@ -17,3 +17,5 @@ val instantiate_tac_by_name : Id.t ->
Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic
val let_evar : Name.t -> EConstr.types -> unit Proofview.tactic
+
+val hget_evar : int -> unit Proofview.tactic
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index f8db0b4fcd..53b726432c 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -177,7 +177,7 @@ ARGUMENT EXTEND lglob
END
let interp_casted_constr ist gl c =
- interp_constr_gen (Pretyping.OfType (EConstr.of_constr (pf_concl gl))) ist (pf_env gl) (project gl) c
+ interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
ARGUMENT EXTEND casted_constr
TYPED AS constr
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 65c75703b5..519633bbed 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -693,24 +693,8 @@ END
hget_evar
*)
-let hget_evar n =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma = Tacmach.New.project gl in
- let concl = Proofview.Goal.concl gl in
- let concl = EConstr.Unsafe.to_constr concl in
- let evl = evar_list concl in
- let concl = EConstr.of_constr concl 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 = (fst ev, Array.map EConstr.of_constr (snd ev)) in
- let ev_type = existential_type sigma ev in
- change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
- end }
-
TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> [ hget_evar n ]
+| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ]
END
(**********************************************************************)
@@ -747,7 +731,6 @@ let refl_equal =
let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
- let type_of_a = EConstr.of_constr type_of_a in
Tacticals.New.tclTHENLIST
[Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -804,7 +787,6 @@ let destauto t =
let destauto_in id =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
- let ctype = EConstr.of_constr ctype in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
@@ -1088,7 +1070,7 @@ END
VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
- let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in
+ let it c = EConstr.Unsafe.to_constr (snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c)) in
let k1 = Keys.constr_key (it c) in
let k2 = Keys.constr_key (it c') in
match k1, k2 with
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 3c6bd45637..715929c562 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -135,7 +135,6 @@ let app_poly_check env evars f args =
let (evars, cstrs), fc = f evars in
let evdref = ref evars in
let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
- let t = EConstr.of_constr t in
(!evdref, cstrs), t
let app_poly_nocheck env evars f args =
@@ -509,7 +508,6 @@ let rec decompose_app_rel env evd t =
| App (f, [|arg|]) ->
let (f', argl, argr) = decompose_app_rel env evd arg in
let ty = Typing.unsafe_type_of env evd argl in
- let ty = EConstr.of_constr ty in
let f'' = mkLambda (Name default_dependent_ident, ty,
mkLambda (Name (Id.of_string "y"), lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -813,7 +811,6 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
- let appmtype = EConstr.of_constr appmtype in
let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs')
@@ -1445,7 +1442,6 @@ module Strategies =
fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
- let c = EConstr.of_constr c in
let unfolded =
try Tacred.try_red_product env sigma c
with e when CErrors.noncritical e ->
@@ -1693,7 +1689,6 @@ let cl_rewrite_clause_strat strat clause =
let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
let (sigma, c) = Pretyping.understand_tcc env sigma c in
- let c = EConstr.of_constr c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
@@ -1702,7 +1697,6 @@ let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input)
let interp_glob_constr_list env =
let make c = (); fun sigma ->
let sigma, c = Pretyping.understand_tcc env sigma c in
- let c = EConstr.of_constr c in
(sigma, (c, NoBindings))
in
List.map (fun c -> make c, true, None)
@@ -1940,7 +1934,6 @@ let build_morphism_signature env sigma m =
let m = EConstr.of_constr m in
let sigma = Evd.from_ctx ctx in
let t = Typing.unsafe_type_of env sigma m in
- let t = EConstr.of_constr t in
let cstrs =
let rec aux t =
match EConstr.kind sigma t with
@@ -1971,7 +1964,6 @@ let default_morphism sign m =
let env = Global.env () in
let sigma = Evd.from_env env in
let t = Typing.unsafe_type_of env sigma m in
- let t = EConstr.of_constr t in
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
@@ -2111,7 +2103,7 @@ let get_hyp gl (c,l) clause l2r =
let env = Tacmach.New.pf_env gl in
let sigma, hi = decompose_applied_relation env evars (c,l) in
let but = match clause with
- | Some id -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl)
+ | Some id -> Tacmach.New.pf_get_hyp_typ id gl
| None -> nf_evar evars (Tacmach.New.pf_concl gl)
in
unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
@@ -2228,7 +2220,6 @@ let setoid_symmetry_in id =
Proofview.V82.tactic (fun gl ->
let sigma = project gl in
let ctype = pf_unsafe_type_of gl (mkVar id) in
- let ctype = EConstr.of_constr ctype in
let binders,concl = decompose_prod_assum sigma ctype in
let (equiv, args) = decompose_app sigma concl in
let rec split_last_two = function
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d8df07733f..36a0336bca 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -636,7 +636,6 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) c
in
- let c = EConstr.of_constr c in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
@@ -795,7 +794,6 @@ let interp_may_eval f ist env sigma = function
let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
- let c = EConstr.of_constr c in
!evdref , c
with
| Not_found ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-08 22:58:19 +0000