diff options
31 files changed, 83 insertions, 118 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 204997445..73286f2c4 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -611,6 +611,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = (nhyps,terms) let clear_hyps_in_evi env evdref hyps concl ids = + let concl = EConstr.Unsafe.to_constr concl in match clear_hyps_in_evi_main env evdref hyps [concl] ids with | (nhyps,[nconcl]) -> (nhyps,nconcl) | _ -> assert false diff --git a/engine/evarutil.mli b/engine/evarutil.mli index cf36f5953..5882f02b9 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -199,7 +199,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) val cleared : bool Store.field -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> +val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> EConstr.types -> Id.Set.t -> named_context_val * types val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> diff --git a/engine/proofview.ml b/engine/proofview.ml index 9adf94744..9e5e9c7da 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -984,7 +984,7 @@ module Goal = struct type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; - concl : Term.constr ; + concl : EConstr.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } @@ -1005,7 +1005,7 @@ module Goal = struct let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; - concl = Evd.evar_concl info ; + concl = EConstr.of_constr (Evd.evar_concl info); self = goal } let nf_gmake env sigma goal = diff --git a/engine/proofview.mli b/engine/proofview.mli index 725445251..2350592a2 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -484,7 +484,7 @@ module Goal : sig respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> Term.constr + val concl : ([ `NF ], 'r) t -> EConstr.constr val hyps : ([ `NF ], 'r) t -> Context.Named.t val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t @@ -492,7 +492,7 @@ module Goal : sig (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : ('a, 'r) t -> Term.constr + val raw_concl : ('a, 'r) t -> EConstr.constr type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d53248a04..188d041c1 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -355,7 +355,7 @@ let refine_tac ist simple c = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = constr_flags in - let expected_type = Pretyping.OfType (EConstr.of_constr concl) in + let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> let Sigma (c, sigma, p) = c.delayed env sigma in @@ -647,7 +647,6 @@ let hResolve id c occ t = let sigma = Sigma.to_evar_map sigma in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env_ids = Termops.ids_of_context env in let c_raw = Detyping.detype true env_ids env sigma c in let t_raw = Detyping.detype true env_ids env sigma t in @@ -694,6 +693,7 @@ 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 @@ -748,7 +748,6 @@ let mkCaseEq a : unit Proofview.tactic = [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in 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 @@ -761,14 +760,14 @@ let mkCaseEq a : unit Proofview.tactic = let case_eq_intros_rewrite x = Proofview.Goal.nf_enter { enter = begin fun gl -> - let n = nb_prod (Tacmach.New.project gl) (EConstr.of_constr (Proofview.Goal.concl gl)) in + let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in - let n' = nb_prod (Tacmach.New.project gl) (EConstr.of_constr concl) in + let n' = nb_prod (Tacmach.New.project gl) concl in let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO (n'-n-1) intro; @@ -809,7 +808,7 @@ let destauto_in id = end } TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (EConstr.of_constr (Proofview.Goal.concl gl)) end } ] +| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index d4b84284f..a983a4fea 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -92,12 +92,10 @@ let rec eq_constr_mod_evars sigma x y = let progress_evars t = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let check = Proofview.Goal.nf_enter { enter = begin fun gl' -> let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in - let newconcl = EConstr.of_constr newconcl in if eq_constr_mod_evars sigma concl newconcl then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 119e872f8..4c350b093 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1595,7 +1595,6 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with let assert_replacing id newt tac = let prf = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ctx = Environ.named_context env in @@ -1665,7 +1664,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = match clause with @@ -2143,10 +2141,9 @@ 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 -> Tacmach.New.pf_get_hyp_typ id gl - | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl) + | Some id -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) + | None -> nf_evar evars (Tacmach.New.pf_concl gl) in - let but = EConstr.of_constr but in unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } @@ -2195,7 +2192,6 @@ let setoid_proof ty fn fallback = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in Proofview.tclORELSE begin try diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 3ed40357e..572fa32b7 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1536,7 +1536,6 @@ and interp_match_goal ist lz lr lmr = let hyps = Proofview.Goal.hyps gl in let hyps = if lr then List.rev hyps else hyps in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) end } diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index 5cbddc7f6..be1123d5c 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -51,6 +51,7 @@ let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let penv = print_named_context env in + let concl = EConstr.Unsafe.to_constr concl in let pc = print_constr_env env concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 4d2859fb0..93bd88fe4 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -221,6 +221,7 @@ module Btauto = struct Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in + let concl = EConstr.Unsafe.to_constr concl in let t = decomp_term (Tacmach.New.project gl) concl in match t with | Term.App (c, [|typ; p; _|]) when c === eq -> @@ -235,6 +236,7 @@ module Btauto = struct let tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6295e004e..130f01e97 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -230,7 +230,7 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let ci= (snd(fst cstr)) in - let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in + let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) default in let body = EConstr.Unsafe.to_constr body in let id=pf_get_new_id (Id.of_string "t") gls in mkLambda(Name id,intype,body) @@ -321,6 +321,7 @@ let rec proof_tac p : unit Proofview.tactic = let special=mkRel (1+nargs-argind) in refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> + let default = EConstr.of_constr default in let proj = Tacmach.New.of_old (build_projection intype cstr special default) gl in @@ -388,6 +389,7 @@ let discriminate_tac (cstr,u as cstru) p = let pred = mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in + let concl = EConstr.Unsafe.to_constr concl in let injt=app_global _f_equal [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = @@ -498,6 +500,7 @@ let mk_eq f c1 c2 k = let f_equal = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let concl = EConstr.Unsafe.to_constr concl in let cut_eq c1 c2 = try (* type_of can raise an exception *) Tacticals.New.tclTHENS diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e73166be2..c3254010a 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -41,7 +41,7 @@ let clear ids { it = goal; sigma } = let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in let env = Goal.V82.env sigma goal in let sign = Goal.V82.hyps sigma goal in - let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in + let cl = Goal.V82.concl sigma goal in let evdref = ref (Evd.clear_metas sigma) in let (hyps, concl) = try Evarutil.clear_hyps_in_evi env evdref sign cl ids diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index f9802ee5e..bffca6223 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -470,7 +470,7 @@ let rec fourier () = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in + let goal = Termops.strip_outer_cast sigma concl in let goal = EConstr.Unsafe.to_constr goal in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f39549514..72290e681 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1857,6 +1857,7 @@ let destructure_goal = in Tacticals.New.tclTHEN goal_tac destructure_hyps in + let concl = EConstr.Unsafe.to_constr concl in (loop concl) end } diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 04a747fb4..5f8a0b2d5 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -452,6 +452,7 @@ let quote f lid = let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in let ivs = compute_ivs f cl gl in let concl = Proofview.Goal.concl gl in + let concl = EConstr.Unsafe.to_constr concl in let quoted_terms = quote_terms ivs [concl] in let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index aa91494eb..d34c9325e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1078,7 +1078,7 @@ END let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in - let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in + let cl = Goal.V82.concl sigma goal in let evdref = ref (Evd.clear_metas sigma) in let ans = try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 84cdc09ee..32c887ff5 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -144,7 +144,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let evd = clear_metas (Tacmach.New.project gl) in try - let evd' = w_unify env evd CONV ~flags m (EConstr.of_constr n) in + let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end } diff --git a/proofs/refine.ml b/proofs/refine.ml index 11eabe0a9..32064aff5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -77,7 +77,6 @@ let make_refine_enter ?(unsafe = true) f = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -146,7 +145,6 @@ let with_type env evd c t = let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let f = { run = fun h -> let Sigma (c, h, p) = f.run h in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index aa54e4f9b..f3f19e854 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -220,7 +220,7 @@ module New = struct let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in - nf_evar sigma concl + EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl)) let pf_whd_all gl t = pf_apply whd_all gl t @@ -229,13 +229,13 @@ module New = struct let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t) let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t + let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t) let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 340c7addc..7b387ac9a 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -106,7 +106,7 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types @@ -120,13 +120,13 @@ module New : sig val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types - val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map diff --git a/tactics/auto.ml b/tactics/auto.ml index 21fe9667b..4218be0bb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -331,7 +331,6 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = in Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in - let concl = EConstr.of_constr concl in let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in Tacticals.New.tclFIRST @@ -492,7 +491,6 @@ let search d n mod_delta db_list local_db = (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in - let concl = EConstr.of_constr concl in let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in let d' = incr_dbg d in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6c45bef1c..bf4e53b10 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -249,7 +249,6 @@ let unify_resolve_refine poly flags = { enter = begin fun gls ((c, t, ctx),n,clenv) -> let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in - let concl = EConstr.of_constr concl in Refine.refine ~unsafe:true { Sigma.run = fun sigma -> let sigma = Sigma.to_evar_map sigma in let sigma, term, ty = @@ -363,7 +362,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars = Proofview.Goal.nf_enter { enter = begin fun gl -> let tacs = e_trivial_resolve db_list local_db secvars only_classes - (project gl) (EConstr.of_constr (pf_concl gl)) in + (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) end} in @@ -1002,7 +1001,6 @@ module Search = struct let open Proofview.Notations in let env = Goal.env gl in let concl = Goal.concl gl in - let concl = EConstr.of_constr concl in let sigma = Goal.sigma gl in let s = Sigma.to_evar_map sigma in let unique = not info.search_dep || is_unique env s concl in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 986d1a624..57400d334 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -34,7 +34,6 @@ let e_give_exact ?(flags=eauto_unif_flags) c = 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 t2 = EConstr.of_constr t2 in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) @@ -151,7 +150,7 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (EConstr.of_constr (Tacmach.New.pf_nf_concl gl)))) + (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end } @@ -508,7 +507,6 @@ let autounfold_one db cl = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let st = List.fold_left (fun (i,c) dbname -> let db = try searchtable_map dbname diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index a96656d3a..16e0d9684 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -178,7 +178,6 @@ let solveEqBranch rectype = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - let concl = EConstr.of_constr concl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in @@ -205,7 +204,6 @@ let decideGralEquality = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - let concl = EConstr.of_constr concl in let sigma = project gl in match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app sigma (pf_compute gl typ) in diff --git a/tactics/equality.ml b/tactics/equality.ml index 2eead2d22..209c9eb66 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -312,9 +312,8 @@ 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 -> pf_get_hyp_typ id (Proofview.Goal.assume gl) + | Some id -> EConstr.of_constr (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let typ = EConstr.of_constr typ in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) else tclMAP try_clause cs @@ -409,7 +408,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 -> pf_get_hyp_typ id gl + | Some id -> EConstr.of_constr (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 -> @@ -417,7 +416,6 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in - let type_of_cls = EConstr.of_constr type_of_cls in let dep = dep_proof_ok && dep_fun evd c type_of_cls in let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in let tac = @@ -1052,7 +1050,6 @@ let onNegatedEquality with_evars tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let ccl = Proofview.Goal.concl gl in - let ccl = EConstr.of_constr ccl in let env = Proofview.Goal.env gl in match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with | Prod (_,t,u) when is_empty_type sigma u -> @@ -1611,7 +1608,6 @@ let cutSubstInConcl l2r eqn = let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_concl 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 = @@ -1752,7 +1748,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env sigma x (EConstr.of_constr concl) in + let depconcl = occur_var env sigma x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b92d65908..fa114a3d3 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -468,7 +468,6 @@ let match_eq_nf gls eqn (ref, hetero) = let n = if hetero then 4 else 3 in let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in let pat = mkPattern (mkGAppRef ref args) in - let pf_whd_all gls c = EConstr.of_constr (pf_whd_all gls c) in match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); diff --git a/tactics/inv.ml b/tactics/inv.ml index ac9a564e5..e45eb2a16 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -34,7 +34,7 @@ module NamedDecl = Context.Named.Declaration let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in let sigma = project gl in - occur_var env sigma id (EConstr.of_constr (Proofview.Goal.concl gl)) || + occur_var env sigma id (Proofview.Goal.concl gl) || List.exists (occur_var_in_decl env sigma id) (Proofview.Goal.hyps gl) (* [make_inv_predicate (ity,args) C] @@ -441,7 +441,6 @@ let raw_inversion inv_kind id status names = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl 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)) @@ -522,13 +521,13 @@ let invIn k names ids id = let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in let sigma = project gl in - let nb_prod_init = nb_prod sigma (EConstr.of_constr concl) in + let nb_prod_init = nb_prod sigma concl in let intros_replace_ids = Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in let sigma = project gl in let nb_of_new_hyp = - nb_prod sigma (EConstr.of_constr concl) - (List.length hyps + nb_prod_init) + nb_prod sigma concl - (List.length hyps + nb_prod_init) in if nb_of_new_hyp < 1 then intros_replacing ids diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 62e78b588..609fa1be8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -294,7 +294,7 @@ let lemInvIn id c ids = let intros_replace_ids = let concl = Proofview.Goal.concl gl in let sigma = project gl in - let nb_of_new_hyp = nb_prod sigma (EConstr.of_constr concl) - List.length ids in + let nb_of_new_hyp = nb_prod sigma concl - List.length ids in if nb_of_new_hyp < 1 then intros_replacing ids else diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e440f1dc5..d79a74b36 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -710,7 +710,7 @@ module New = struct let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) let c = Proofview.Goal.concl (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_hyp id gl = (** Retyping will expand evars anyway. *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 03f81773b..dabe78b34 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -207,7 +207,6 @@ let introduction ?(check=true) id = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in let store = Proofview.Goal.extra gl in @@ -230,7 +229,6 @@ let convert_concl ?(check=true) ty k = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in - let conclty = EConstr.of_constr conclty in Refine.refine ~unsafe:true { run = begin fun sigma -> let Sigma ((), sigma, p) = if check then begin @@ -251,7 +249,6 @@ let convert_hyp ?(check=true) d = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.raw_concl gl in - let ty = EConstr.of_constr ty in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in @@ -353,7 +350,6 @@ let move_hyp id dest = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.raw_concl gl in - let ty = EConstr.of_constr ty in let store = Proofview.Goal.extra gl in let sign = named_context_val env in let sign' = move_hyp_in_named_context sigma id dest sign in @@ -409,6 +405,7 @@ let rename_hyp repl = |> NamedDecl.map_constr subst in let nhyps = List.map map hyps in + let concl = EConstr.Unsafe.to_constr concl in let nconcl = subst concl in let nconcl = EConstr.of_constr nconcl in let nctx = Environ.val_of_named_context nhyps in @@ -545,7 +542,6 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let (sp, u) = check_mutind env sigma n concl in let firsts, lasts = List.chop j rest in let all = firsts @ (f, n, concl) :: lasts in @@ -601,7 +597,6 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let firsts,lasts = List.chop j others in let all = firsts @ (f, concl) :: lasts in List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all; @@ -727,7 +722,7 @@ let bind_red_expr_occurrences occs nbcl redexp = let reduct_in_concl (redfun,sty) = Proofview.Goal.nf_enter { enter = begin fun gl -> - convert_concl_no_check (EConstr.of_constr (Tacmach.New.pf_apply redfun gl (EConstr.of_constr (Tacmach.New.pf_concl gl)))) sty + convert_concl_no_check (EConstr.of_constr (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl))) sty end } let reduct_in_hyp ?(check=false) redfun (id,where) = @@ -762,7 +757,7 @@ let pf_e_reduce_decl redfun where decl gl = let e_reduct_in_concl ~check (redfun, sty) = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (EConstr.of_constr (Tacmach.New.pf_concl gl)) in + let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in let c' = EConstr.of_constr c' in Sigma (convert_concl ~check c' sty, sigma, p) end } @@ -783,7 +778,7 @@ let e_reduct_option ?(check=false) redfun = function let e_change_in_concl (redfun,sty) = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (EConstr.of_constr (Proofview.Goal.raw_concl gl)) in + let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in let c = EConstr.of_constr c in Sigma (convert_concl_no_check c sty, sigma, p) end } @@ -976,7 +971,6 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = EConstr.of_constr concl in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (local_assum (name,t)) name_flag gl in @@ -1120,7 +1114,7 @@ let lookup_hypothesis_as_renamed_gen red h gl = aux c | x -> x in - try aux (Proofview.Goal.concl gl) + try aux (EConstr.to_constr (Tacmach.New.project gl) (Proofview.Goal.concl gl)) with Redelimination -> None let is_quantified_hypothesis id gl = @@ -1261,7 +1255,6 @@ let cut c = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_nf_concl gl in - let concl = EConstr.of_constr concl in let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) @@ -1302,7 +1295,7 @@ let check_unresolved_evars_of_metas sigma clenv = (match kind_of_term c.rebus with | Evar (evk,_) when Evd.is_undefined clenv.evd evk && not (Evd.mem sigma evk) -> - error_uninstantiated_metas (EConstr.mkMeta mv) clenv + error_uninstantiated_metas (mkMeta mv) clenv | _ -> ()) | _ -> ()) (meta_list clenv.evd) @@ -1401,7 +1394,6 @@ let enforce_prop_bound_names rename tac = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in - let t = EConstr.of_constr t in change_concl (aux env sigma i t) end } in (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) @@ -1487,7 +1479,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in let Sigma (elim, sigma, p) = - if occur_term (Sigma.to_evar_map sigma) c (EConstr.of_constr concl) then + if occur_term (Sigma.to_evar_map sigma) c concl then build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in @@ -1728,7 +1720,6 @@ let solve_remaining_apply_goals = let env = Proofview.Goal.env gl in let evd = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in if Typeclasses.is_class_type evd concl then let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in @@ -1755,7 +1746,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod_modulo_zeta sigma (EConstr.of_constr concl) in + let concl_nprod = nb_prod_modulo_zeta sigma concl in let rec try_main_apply with_destruct c = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -1966,10 +1957,9 @@ 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 (EConstr.of_constr (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 (EConstr.of_constr (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 concl = EConstr.of_constr concl in let env = Tacmach.New.pf_env gl in Refine.refine { run = begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in @@ -1999,7 +1989,6 @@ let exact_check c = let sigma = Proofview.Goal.sigma gl in (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in @@ -2013,8 +2002,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = EConstr.of_constr concl in - exact_no_check (EConstr.mkCast (c, cast, concl)) + exact_no_check (mkCast (c, cast, concl)) end } let vm_cast_no_check c = cast_no_check Term.VMcast c @@ -2025,7 +2013,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 (pf_concl gl) in + let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (EConstr.Unsafe.to_constr (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) @@ -2041,13 +2029,14 @@ let assumption = else Tacticals.New.tclZEROMSG (str "No such assumption.") | decl::rest -> let t = NamedDecl.get_type decl in + let t = EConstr.of_constr t in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = - if only_eq then (sigma, Constr.equal t concl) + if only_eq then (sigma, EConstr.eq_constr sigma t concl) else let env = Proofview.Goal.env gl in - infer_conv env sigma (EConstr.of_constr t) (EConstr.of_constr concl) + infer_conv env sigma t concl in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> @@ -2099,7 +2088,6 @@ let clear_body ids = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let concl = EConstr.of_constr concl in let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function @@ -2173,7 +2161,7 @@ let keep hyps = let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env sigma hyp) keep - || occur_var env sigma hyp (EConstr.of_constr ccl) + || occur_var env sigma hyp ccl then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (Proofview.Goal.env gl) @@ -2213,7 +2201,6 @@ let bring_hyps hyps = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let concl = Tacmach.New.pf_nf_concl gl in - let concl = EConstr.of_constr concl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.map_of_list EConstr.of_constr (Context.Named.to_instance hyps) in Refine.refine { run = begin fun sigma -> @@ -2251,7 +2238,6 @@ let constructor_tac with_evars expctdnumopt i lbind = let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in - let cl = EConstr.of_constr cl in let (mind,redcl) = reduce_to_quantified_ind cl in let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in @@ -2291,7 +2277,6 @@ let any_constructor with_evars tacopt = let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in - let cl = EConstr.of_constr cl in let mind = fst (reduce_to_quantified_ind cl) in let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in @@ -2768,7 +2753,6 @@ let letin_tac with_eq id c ty occs = let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in let abs = AbstractExact (id,c,ty,occs,true) in - let ccl = EConstr.of_constr ccl in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in (* We keep the original term to match but record the potential side-effects of unifying universes. *) @@ -2787,7 +2771,6 @@ let letin_pat_tac with_eq id c occs = let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in - let ccl = EConstr.of_constr ccl in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in let Sigma (c, sigma, p) = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c @@ -2921,7 +2904,7 @@ let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun let env = Proofview.Goal.env gl in let newcl, evd = List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr - (EConstr.of_constr (Tacmach.New.pf_concl gl),Tacmach.New.project gl) + (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in @@ -2934,7 +2917,6 @@ let new_generalize_gen_let lconstr = let sigma = Proofview.Goal.sigma gl in let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let concl = EConstr.of_constr concl in let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in @@ -3475,8 +3457,8 @@ let cook_sign hyp0_opt inhyps indvars env sigma = (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: EConstr.constr with_bindings option; - elimt: EConstr.types; + elimc: constr with_bindings option; + elimt: types; indref: global_reference option; params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) @@ -3488,7 +3470,7 @@ type elim_scheme = { nargs: int; (* number of arguments *) indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) - concl: EConstr.types; (* Qi x1...xni HI (f...), HI and (f...) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) @@ -3497,7 +3479,7 @@ type elim_scheme = { let empty_scheme = { elimc = None; - elimt = EConstr.mkProp; + elimt = mkProp; indref = None; params = []; nparams = 0; @@ -3508,7 +3490,7 @@ let empty_scheme = args = []; nargs = 0; indarg = None; - concl = EConstr.mkProp; + concl = mkProp; indarg_in_concl = false; farg_in_concl = false; } @@ -3582,7 +3564,7 @@ let lift_togethern n l = l ([], n) in l' -let lift_list l = List.map (EConstr.Vars.lift 1) l +let lift_list l = List.map (lift 1) l let ids_of_constr sigma ?(all=false) vars c = let rec aux vars c = @@ -4251,7 +4233,6 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in let concl = Tacmach.New.pf_nf_concl gl in - let concl = EConstr.of_constr concl in let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in let dep = dep_in_hyps || dep_in_concl in @@ -4341,7 +4322,7 @@ let induction_without_atomization isrec with_evars elim names lid = (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = Proofview.Goal.nf_enter { enter = begin fun gl -> - if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (EConstr.of_constr (Tacmach.New.pf_concl gl)) && + if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then user_err (str "Conclusion must be mentioned: it depends on " ++ pr_id id @@ -4437,7 +4418,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let check = check_enough_applied env sigma elim in let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in - let ccl = EConstr.of_constr ccl in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with | None -> @@ -4492,7 +4472,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let has_generic_occurrences_but_goal cls id env sigma ccl = clause_with_generic_context_selection cls && (* TODO: whd_evar of goal *) - (cls.concl_occs != NoOccurrences || not (occur_var env sigma id (EConstr.of_constr ccl))) + (cls.concl_occs != NoOccurrences || not (occur_var env sigma id ccl)) let induction_gen clear_flag isrec with_evars elim ((_pending,(c,lbind)),(eqname,names) as arg) cls = @@ -4736,7 +4716,7 @@ let maybe_betadeltaiota_concl allowred gl = if not allowred then concl else let env = Proofview.Goal.env gl in - whd_all env sigma (EConstr.of_constr concl) + EConstr.of_constr (whd_all env sigma concl) let reflexivity_red allowred = Proofview.Goal.enter { enter = begin fun gl -> @@ -4745,7 +4725,6 @@ let reflexivity_red allowred = inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - let concl = EConstr.of_constr concl in match match_with_equality_type sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings @@ -4797,7 +4776,6 @@ let symmetry_red allowred = inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - let concl = EConstr.of_constr concl in match_with_equation sigma concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> @@ -4895,7 +4873,6 @@ let transitivity_red allowred t = inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - let concl = EConstr.of_constr concl in match_with_equation sigma concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> @@ -5003,7 +4980,7 @@ let abstract_subproof id gk tac = else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in - let concl = it_mkNamedProd_or_LetIn (EConstr.of_constr (Proofview.Goal.concl gl)) sign in + let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in let concl = try flush_and_check_evars !evdref concl with Uninstantiated_evar _ -> diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f8ca8343c..5f33ae834 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -338,8 +338,6 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) let do_replace_lb mode lb_scheme_key aavoid narg p q = - let p = EConstr.of_constr p in - let q = EConstr.of_constr q in let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -399,6 +397,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = + let lft = EConstr.Unsafe.to_constr lft in + let rgt = EConstr.Unsafe.to_constr rgt in let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -612,11 +612,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.nf_enter { enter = begin fun gls -> - let gl = Proofview.Goal.concl gls in - match (kind_of_term gl) with + Proofview.Goal.nf_enter { enter = begin fun gl -> + let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in + match EConstr.kind sigma concl with | App (c,ca) -> ( - match (kind_of_term c) with + match EConstr.kind sigma c with | Ind (indeq, u) -> if eq_gr (IndRef indeq) Coqlib.glob_eq then @@ -708,6 +709,7 @@ let compute_lb_goal ind lnamesparrec nparrec = ))), eff let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = + let open EConstr in let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -745,10 +747,11 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = simplest_split ;Auto.default_auto ] ); Proofview.Goal.nf_enter { enter = begin fun gls -> - let gl = Proofview.Goal.concl gls in + let concl = Proofview.Goal.concl gls in + let sigma = Tacmach.New.project gl in (* assume the goal to be eq (eq_type ...) = true *) - match (kind_of_term gl) with - | App(c,ca) -> (match (kind_of_term ca.(1)) with + match EConstr.kind sigma concl with + | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with | App(c',ca') -> let n = Array.length ca' in do_replace_lb mode lb_scheme_key |