aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml11
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/contradiction.ml1
-rw-r--r--tactics/eauto.ml5
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/equality.ml20
-rw-r--r--tactics/hints.ml3
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml1
-rw-r--r--tactics/tacticals.ml22
-rw-r--r--tactics/tactics.ml34
13 files changed, 38 insertions, 71 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f2e98ee01..f43f4b250 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -257,7 +257,7 @@ type hypinfo = {
let decompose_applied_relation metas env sigma c ctype left2right =
let find_rel ty =
- let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in
+ let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
let eqclause =
if metas then eqclause
else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
@@ -274,6 +274,8 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let ty1, ty2 =
Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
in
+ let ty = EConstr.Unsafe.to_constr ty in
+ let ty1 = EConstr.Unsafe.to_constr ty1 in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
@@ -284,9 +286,8 @@ let decompose_applied_relation metas env sigma c ctype left2right =
match find_rel ctype with
| Some c -> Some c
| None ->
- let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
- let t' = EConstr.Unsafe.to_constr t' in
- match find_rel (Term.it_mkProd_or_LetIn t' ctx) with
+ let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+ match find_rel (it_mkProd_or_LetIn t' ctx) with
| Some c -> Some c
| None -> None
@@ -296,7 +297,7 @@ let find_applied_relation metas loc env sigma c left2right =
| Some c -> c
| None ->
user_err ~loc ~hdr:"decompose_applied_relation"
- (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++
+ (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
spc () ++ str"of this term does not end with an applied relation.")
(* To add rewriting rules to a base *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 84ca0aa8f..fa2c21ac3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -227,7 +227,6 @@ let e_give_exact flags poly (c,clenv) gl =
else c, gl
in
let t1 = pf_unsafe_type_of gl c in
- let t1 = EConstr.of_constr t1 in
Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
@@ -1515,7 +1514,6 @@ let autoapply c i gl =
let flags = auto_unif_flags Evar.Set.empty
(Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
let cty = pf_unsafe_type_of gl c in
- let cty = EConstr.of_constr cty in
let ce = mk_clenv_from gl (c,cty) in
let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
((c,cty,Univ.ContextSet.empty),0,ce) } in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index afc7e1547..a3a448aad 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -116,7 +116,6 @@ let contradiction_term (c,lbind as cl) =
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let typ = type_of c in
- let typ = EConstr.of_constr typ in
let _, ccl = splay_prod env sigma typ in
if is_empty_type sigma ccl then
Tacticals.New.tclTHEN
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 92e59c5ce..01f21910c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,7 +32,6 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
Proofview.Goal.enter { enter = begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
- let t1 = EConstr.of_constr t1 in
let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
let sigma = Tacmach.New.project gl in
if occur_existential sigma t1 || occur_existential sigma t2 then
@@ -290,7 +289,7 @@ module SearchProblem = struct
in
let rec_tacs =
let l =
- let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+ let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in
let concl = EConstr.of_constr concl in
filter_tactics s.tacres
(e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
@@ -516,7 +515,7 @@ let autounfold_one db cl =
(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
in
let did, c' = unfold_head env sigma st
- (match cl with Some (id, _) -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) | None -> concl)
+ (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl)
in
if did then
match cl with
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ef848c2e1..a4158f821 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -82,7 +82,6 @@ let general_decompose recognizer c =
let type_of = pf_unsafe_type_of gl in
let sigma = project gl in
let typc = type_of c in
- let typc = EConstr.of_constr typc in
tclTHENS (cut typc)
[ tclTHEN (intro_using tmphyp_name)
(onLastHypId
@@ -136,7 +135,6 @@ let induction_trailer abs_i abs_j bargs =
(fun id ->
Proofview.Goal.nf_enter { enter = begin fun gl ->
let idty = pf_unsafe_type_of gl (mkVar id) in
- let idty = EConstr.of_constr idty in
let fvty = global_vars (pf_env gl) (project gl) idty in
let possible_bring_hyps =
(List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 16e0d9684..df60f2c66 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -163,7 +163,6 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
| a1 :: largs, a2 :: rargs ->
Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl a1 in
- let rectype = EConstr.of_constr rectype in
let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
let subtacs =
@@ -236,7 +235,6 @@ let decideEquality rectype =
let compare c1 c2 =
Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl c1 in
- let rectype = EConstr.of_constr rectype in
let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
(tclTHENS (cut decide)
[(tclTHEN intro
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e1c39bb34..7dcfd419e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -311,7 +311,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
in
let typ = match cls with
| None -> pf_nf_concl gl
- | Some id -> EConstr.of_constr (pf_get_hyp_typ id (Proofview.Goal.assume gl))
+ | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
in
let cs = instantiate_lemma typ in
if firstonly then tclFIRST (List.map try_clause cs)
@@ -407,7 +407,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
let type_of_clause cls gl = match cls with
| None -> Proofview.Goal.concl gl
- | Some id -> EConstr.of_constr (pf_get_hyp_typ id gl)
+ | Some id -> pf_get_hyp_typ id gl
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
@@ -950,7 +950,6 @@ let gen_absurdity id =
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
- let hyp_typ = EConstr.of_constr hyp_typ in
if is_empty_type sigma hyp_typ
then
simplest_elim (mkVar id)
@@ -1027,7 +1026,6 @@ let onEquality with_evars tac (c,lbindc) =
let type_of = pf_unsafe_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
let t = type_of c in
- let t = EConstr.of_constr t in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
@@ -1136,7 +1134,7 @@ 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 = Int.Set.union prev_rels direct_rels in
- let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i))))
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
in minimalrec_free_rels_rec Int.Set.empty
@@ -1184,7 +1182,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
(* is the default value typable with the expected type *)
let dflt_typ = unsafe_type_of env sigma dflt in
try
- let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in
+ let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
dflt
with Evarconv.UnableToUnify _ ->
@@ -1200,7 +1198,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
match evopt with
| Some w ->
let w_type = unsafe_type_of env !evdref w in
- let w_type = EConstr.of_constr w_type in
if Evarconv.e_cumul env evdref w_type a then
let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
let exist_term = EConstr.of_constr exist_term in
@@ -1290,7 +1287,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
sigma, (tuple,tuplety,dfltval)
let rec build_injrec env sigma dflt c = function
- | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c))
+ | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
| ((sp,cnum),argnum)::l ->
try
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1345,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty =
if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
- let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in
+ let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
let inj2 = EConstr.of_constr inj2 in
@@ -1613,7 +1610,6 @@ let cutSubstInHyp l2r eqn id =
let sigma = Proofview.Goal.sigma gl in
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
- let typ = EConstr.of_constr typ in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
let tac =
@@ -1702,8 +1698,7 @@ let is_eq_x gl x d =
| Var id' -> Id.equal id id'
| _ -> false
in
- let c = pf_nf_evar gl (NamedDecl.get_type d) in
- let c = EConstr.of_constr c in
+ let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in
let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1852,7 +1847,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
try
- let c = EConstr.of_constr c in
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2446b6996..851e9f01f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -919,7 +919,7 @@ let make_mode ref m =
let make_trivial env sigma poly ?(name=PathAny) r =
let c,ctx = fresh_global_or_constr env sigma poly r in
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+ let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
let hd = head_constr sigma t in
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd, { pri=1;
@@ -1239,7 +1239,6 @@ let interp_hints poly =
let sigma = Evd.from_env env in
let f poly c =
let evd,c = Constrintern.interp_open_constr env sigma c in
- let c = EConstr.of_constr c in
prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
let fref r =
let gr = global_with_alias r in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fa114a3d3..607d6d2a9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -442,7 +442,7 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
let extract_eq_args gl = function
| MonomorphicLeibnizEq (e1,e2) ->
- let t = pf_unsafe_type_of gl e1 in (EConstr.of_constr t,e1,e2)
+ let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
| PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
| HeterogenousEq (t1,e1,t2,e2) ->
if pf_conv_x gl t1 t2 then (t1,e1,e2)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a398e04dd..426749a75 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -346,7 +346,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
let sigma = project gl in
(** We only look at the type of hypothesis "id" *)
let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
- let (t,t1,t2) = Hipattern.dest_nf_eq gl (EConstr.of_constr hyp) in
+ let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
| Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
| _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
@@ -443,7 +443,7 @@ let raw_inversion inv_kind id status names =
let concl = Proofview.Goal.concl gl in
let c = mkVar id in
let (ind, t) =
- try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c))
+ try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
CErrors.user_err msg
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2d59285e6..3199623e7 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -258,7 +258,6 @@ let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () in
let evd = ref (Evd.from_env env) in
let c = Constrintern.interp_type_evars env evd com in
- let c = EConstr.of_constr c in
let sigma, sort = Pretyping.interp_sort !evd comsort in
try
add_inversion_lemma na env sigma c sort bool tac
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d79a74b36..89acc149c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -128,7 +128,7 @@ let onClauseLR tac cl gls =
tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls
let ifOnHyp pred tac1 tac2 id gl =
- if pred (id,EConstr.of_constr (pf_get_hyp_typ gl id)) then
+ if pred (id,pf_get_hyp_typ gl id) then
tac1 id gl
else
tac2 id gl
@@ -248,10 +248,10 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
Array.map2 analrec lc lrecargs
let elimination_sort_of_goal gl =
- pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_concl gl))
+ pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
let elimination_sort_of_hyp id gl =
- pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_get_hyp_typ gl id))
+ pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id)
let elimination_sort_of_clause = function
| None -> elimination_sort_of_goal
@@ -269,21 +269,22 @@ let pf_constr_of_global gr k =
let gl_make_elim ind gl =
let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
- pf_apply Evd.fresh_global gl gr
+ let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+ (sigma, EConstr.of_constr c)
let gl_make_case_dep ind gl =
let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
(elimination_sort_of_goal gl)
in
- (Sigma.to_evar_map sigma, r)
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
let gl_make_case_nodep ind gl =
let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
(elimination_sort_of_goal gl)
in
- (Sigma.to_evar_map sigma, r)
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
let make_elim_branch_assumptions ba gl =
let assums =
@@ -583,7 +584,6 @@ module New = struct
let ifOnHyp pred tac1 tac2 id =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
- let typ = EConstr.of_constr typ in
if pred (id,typ) then
tac1 id
else
@@ -630,7 +630,7 @@ module New = struct
(Proofview.Goal.nf_enter { enter = begin fun gl ->
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
(* applying elimination_scheme just a little modified *)
- let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in
+ let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
let indmv =
match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
@@ -642,7 +642,7 @@ module New = struct
| Meta p -> p
| _ ->
let name_elim =
- match kind_of_term elim with
+ match EConstr.kind sigma elim with
| Const (kn, _) -> string_of_con kn
| Var id -> string_of_id id
| _ -> "\b"
@@ -680,7 +680,7 @@ module New = struct
let elimination_then tac c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c)) in
+ let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
| None -> true,gl_make_elim
@@ -715,7 +715,7 @@ module New = struct
let elimination_sort_of_hyp id gl =
(** Retyping will expand evars anyway. *)
let c = pf_get_hyp_typ id (Goal.assume gl) in
- pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c)
+ pf_apply Retyping.get_sort_family_of gl c
let elimination_sort_of_clause id gl = match id with
| None -> elimination_sort_of_goal gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dcaa15fd8..f79f7f1a8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1260,7 +1260,6 @@ let cut c =
try
(** Backward compat: ensure that [c] is well-typed. *)
let typ = Typing.unsafe_type_of env sigma c in
- let typ = EConstr.of_constr typ in
let typ = whd_all env sigma typ in
match EConstr.kind sigma typ with
| Sort _ -> true
@@ -1515,7 +1514,7 @@ let find_ind_eliminator ind s gl =
evd, c
let find_eliminator c gl =
- let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c)) in
+ let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
if is_nonrec ind then raise IsNonrec;
let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
evd, {elimindex = None; elimbody = (c,NoBindings);
@@ -1891,7 +1890,6 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
- let t' = EConstr.of_constr t' in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (local_assum (Anonymous,t')) naming gl in
let rec aux idstoclear with_destruct c =
@@ -1949,7 +1947,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
let cut_and_apply c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
- match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c))) with
+ match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
| Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
let concl = Proofview.Goal.concl gl in
let env = Tacmach.New.pf_env gl in
@@ -2004,7 +2002,7 @@ let exact_proof c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
Refine.refine { run = begin fun sigma ->
let sigma = Sigma.to_evar_map sigma in
- let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (EConstr.Unsafe.to_constr (pf_concl gl)) in
+ let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
let c = EConstr.of_constr c in
let sigma = Evd.merge_universe_context sigma ctx in
Sigma.Unsafe.of_pair (c, sigma)
@@ -2326,7 +2324,6 @@ let intro_decomp_eq loc l thin tac id =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
- let t = EConstr.of_constr t in
let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
match my_find_eq_data_decompose gl t with
| Some (eq,u,eq_args) ->
@@ -2341,7 +2338,6 @@ let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
Proofview.Goal.enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
- let t = EConstr.of_constr t in
let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
let branchsigns = compute_constructor_signatures false ind in
let nv_with_let = Array.map List.length branchsigns in
@@ -2366,7 +2362,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
let sigma = Tacmach.New.project gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let whd_all = Tacmach.New.pf_apply whd_all gl in
- let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in
+ let t = whd_all (type_of (mkVar id)) in
let eqtac, thin = match match_with_equality_type sigma t with
| Some (hdcncl,[_;lhs;rhs]) ->
if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
@@ -2774,7 +2770,6 @@ let forward b usetac ipat c =
| None ->
Proofview.Goal.enter { enter = begin fun gl ->
let t = Tacmach.New.pf_unsafe_type_of gl c in
- let t = EConstr.of_constr t in
let sigma = Tacmach.New.project gl in
let hd = head_ident sigma c in
Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
@@ -2861,7 +2856,7 @@ let old_generalize_dep ?(with_let=false) c gl =
-> id::tothin
| _ -> tothin
in
- let cl' = it_mkNamedProd_or_LetIn (EConstr.of_constr (Tacmach.pf_concl gl)) to_quantify in
+ let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
let body =
if with_let then
match EConstr.kind sigma c with
@@ -3222,7 +3217,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
- let tmptyp0 = EConstr.of_constr tmptyp0 in
let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
let typ0 = reduce_to_quantified_ref indref tmptyp0 in
let prods, indtyp = decompose_prod_assum sigma typ0 in
@@ -3266,7 +3260,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
| Var id -> id
| _ ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+ id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
@@ -3660,7 +3654,6 @@ let abstract_args gl generalize_vars dep id defined f args =
let sigma = ref (Tacmach.project gl) in
let env = Tacmach.pf_env gl in
let concl = Tacmach.pf_concl gl in
- let concl = EConstr.of_constr concl in
let dep = dep || local_occur_var !sigma id concl in
let avoid = ref [] in
let get_id name =
@@ -3681,7 +3674,6 @@ let abstract_args gl generalize_vars dep id defined f args =
in
let ty = EConstr.of_constr ty in
let argty = Tacmach.pf_unsafe_type_of gl arg in
- let argty = EConstr.of_constr argty in
let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
let () = sigma := sigma' in
let lenctx = List.length ctx in
@@ -3723,7 +3715,6 @@ let abstract_args gl generalize_vars dep id defined f args =
in
if dogen then
let tyf' = Tacmach.pf_unsafe_type_of gl f' in
- let tyf' = EConstr.of_constr tyf' in
let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
in
@@ -3739,7 +3730,6 @@ let abstract_args gl generalize_vars dep id defined f args =
else None, c'
in
let typ = Tacmach.pf_get_hyp_typ gl id in
- let typ = EConstr.of_constr typ in
let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in
let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in
Some (tac, dep, succ (List.length ctx), vars)
@@ -3797,7 +3787,6 @@ let specialize_eqs id gl =
let open Context.Rel.Declaration in
let env = Tacmach.pf_env gl in
let ty = Tacmach.pf_get_hyp_typ gl id in
- let ty = EConstr.of_constr ty in
let evars = ref (project gl) in
let unif env evars c1 c2 =
compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
@@ -4062,7 +4051,6 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
let guess_elim isrec dep s hyp0 gl =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
- let tmptyp0 = EConstr.of_constr tmptyp0 in
let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
let evd, elimc =
if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl
@@ -4080,16 +4068,13 @@ let guess_elim isrec dep s hyp0 gl =
(Sigma.to_evar_map sigma, ind)
in
let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
- let elimt = EConstr.of_constr elimt in
evd, ((elimc, NoBindings), elimt), mkIndU mind
let given_elim hyp0 (elimc,lbind as e) gl =
let sigma = Tacmach.New.project gl in
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
- let tmptyp0 = EConstr.of_constr tmptyp0 in
let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in
let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
- let elimt = EConstr.of_constr elimt in
Tacmach.New.project gl, (e, elimt), ind_type_guess
type scheme_signature =
@@ -4127,7 +4112,7 @@ let get_elim_signature elim hyp0 gl =
let is_functional_induction elimc gl =
let sigma = Tacmach.New.project gl in
- let scheme = compute_elim_sig sigma ~elimc (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (fst elimc))) in
+ let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
(* The test is not safe: with non-functional induction on non-standard
induction scheme, this may fail *)
Option.is_empty scheme.indarg
@@ -4162,7 +4147,6 @@ let recolle_clenv i params args elimclause gl =
arr in
let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
(* parameters correspond to first elts of lid. *)
- let pf_get_hyp_typ id gl = EConstr.of_constr (pf_get_hyp_typ id gl) in
let clauses_params =
List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(i))
0 params in
@@ -4523,7 +4507,7 @@ let induction_gen_l isrec with_evars elim names lc =
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let sigma = Tacmach.New.project gl in
let x =
- id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+ id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in
let id = new_fresh_id [] x gl in
let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
@@ -4778,7 +4762,6 @@ let symmetry_in id =
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
- let ctype = EConstr.of_constr ctype in
let sign,t = decompose_prod_assum sigma ctype in
Proofview.tclORELSE
begin
@@ -4832,7 +4815,6 @@ let prove_transitivity hdcncl eq_kind t =
let sigma = Tacmach.New.project gl in
let type_of = Typing.unsafe_type_of env sigma in
let typt = type_of t in
- let typt = EConstr.of_constr typt in
(mkApp(hdcncl, [| typ1; c1; typt ;t |]),
mkApp(hdcncl, [| typt; t; typ2; c2 |]))
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:43:35 +0000