aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/extratactics.ml417
-rw-r--r--ltac/rewrite.ml19
-rw-r--r--ltac/tacinterp.ml1
3 files changed, 15 insertions, 22 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 188d041c1..138400991 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -290,6 +290,7 @@ END
(* Hint Resolve *)
open Term
+open EConstr
open Vars
open Coqlib
@@ -298,23 +299,26 @@ let project_hint pri l2r r =
let env = Global.env() in
let sigma = Evd.from_env env in
let sigma, c = Evd.fresh_global env sigma gr in
- let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+ let c = EConstr.of_constr c in
+ let t = Retyping.get_type_of env sigma c in
+ let t = EConstr.of_constr t in
let t =
- Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in
- let t = EConstr.Unsafe.to_constr t in
- let sign,ccl = decompose_prod_assum t in
- let (a,b) = match snd (decompose_app ccl) with
+ Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+ let sign,ccl = decompose_prod_assum sigma t in
+ let (a,b) = match snd (decompose_app sigma 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 (EConstr.of_constr (mkApp (c, Context.Rel.to_extended_vect 0 sign))) in
+ let p = EConstr.of_constr p in
+ let c = Reductionops.whd_beta sigma (mkApp (c, Array.map EConstr.of_constr (Context.Rel.to_extended_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
let id =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
let ctx = Evd.universe_context_set sigma in
+ let c = EConstr.to_constr sigma c in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
(pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
@@ -751,7 +755,6 @@ let mkCaseEq a : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
(** FIXME: this looks really wrong. Does anybody really use this tactic? *)
let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in
- let c = EConstr.of_constr c in
change_concl c
end };
simplest_case a]
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 4c350b093..c92ddf990 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -247,14 +247,11 @@ end) = struct
in
let rec aux env evars ty l =
let t = Reductionops.whd_all env (goalevars evars) ty in
- let t = EConstr.of_constr t in
match EConstr.kind (goalevars evars) t, l with
| Prod (na, ty, b), obj :: cstrs ->
let b = Reductionops.nf_betaiota (goalevars evars) b in
- let b = EConstr.of_constr b in
if noccurn (goalevars evars) 1 b (* non-dependent product *) then
let ty = Reductionops.nf_betaiota (goalevars evars) ty in
- let ty = EConstr.of_constr ty in
let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
let evars, relty = mk_relty evars env ty obj in
let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
@@ -264,7 +261,6 @@ end) = struct
aux (Environ.push_rel (local_assum (na, ty)) env) evars b cstrs
in
let ty = Reductionops.nf_betaiota (goalevars evars) ty in
- let ty = EConstr.of_constr ty in
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
@@ -275,7 +271,6 @@ end) = struct
(match finalcstr with
| None | Some (_, None) ->
let t = Reductionops.nf_betaiota (fst evars) ty in
- let t = EConstr.of_constr t in
let evars, rel = mk_relty evars env t None in
evars, t, rel, [t, Some rel]
| Some (t, Some rel) -> evars, t, rel, [t, Some rel])
@@ -355,7 +350,7 @@ end) = struct
if Int.equal n 0 then start evars env prod
else
let sigma = goalevars evars in
- match EConstr.kind sigma (EConstr.of_constr (Reductionops.whd_all env sigma prod)) with
+ match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
| Prod (na, ty, b) ->
if noccurn sigma 1 b then
let b' = lift (-1) b in
@@ -375,7 +370,6 @@ end) = struct
with Not_found ->
let sigma = goalevars evars in
let ty = Reductionops.whd_all env sigma ty in
- let ty = EConstr.of_constr ty in
find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
in find env c ty args
@@ -513,7 +507,6 @@ let error_no_relation () = error "Cannot find a relation to rewrite."
let rec decompose_app_rel env evd t =
(** Head normalize for compatibility with the old meta mechanism *)
let t = Reductionops.whd_betaiota evd t in
- let t = EConstr.of_constr t in
match EConstr.kind evd t with
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
@@ -1011,7 +1004,7 @@ let unfold_match env sigma sk app =
| App (f', args) when eq_constant (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
- EConstr.of_constr (Reductionops.whd_beta sigma (mkApp (v, args)))
+ Reductionops.whd_beta sigma (mkApp (v, args))
| _ -> app
let is_rew_cast = function RewCast _ -> true | _ -> false
@@ -1106,7 +1099,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| x -> x
in
let res =
- { rew_car = EConstr.of_constr (Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args);
+ { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
rew_prf = prf; rew_evars = r.rew_evars }
in
@@ -1455,7 +1448,6 @@ module Strategies =
let rfn, ckind = Redexpr.reduction_of_red_expr env r in
let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in
- let t' = EConstr.of_constr t' in
let evars' = Sigma.to_evar_map sigma in
if Termops.eq_constr evars' t' t then
state, Identity
@@ -1475,7 +1467,6 @@ module Strategies =
with e when CErrors.noncritical e ->
error "fold: the term is not unfoldable !"
in
- let unfolded = EConstr.of_constr unfolded in
try
let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
let c' = nf_evar sigma c in
@@ -1568,7 +1559,6 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| RewCast c -> None
| RewPrf (rel, p) ->
let p = nf_zeta env evars' (nf_evar evars' p) in
- let p = EConstr.of_constr p in
let term =
match abs with
| None -> p
@@ -1951,8 +1941,7 @@ let declare_projection n instance_id r =
| _ -> typ
in aux init
in
- let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ in
- let ccl = EConstr.of_constr ccl
+ let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 572fa32b7..6c59abe66 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -785,6 +785,7 @@ let interp_may_eval f ist env sigma = function
let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma (EConstr.of_constr c_interp) in
+ let c = EConstr.Unsafe.to_constr c in
(Sigma.to_evar_map sigma, c)
| ConstrContext ((loc,s),c) ->
(try
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:50:35 +0000