From a5681c57d82589c2f053d34a687fdd3ed6dc7059 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:35:31 +0100 Subject: unsafe_type_of -> type_of in Eauto.e_give_exact --- tactics/eauto.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 361215bf38..80ca124912 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -32,11 +32,13 @@ let eauto_unif_flags = auto_flags_of_state TransparentState.full let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> - let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let sigma, t1 = Tacmach.New.pf_type_of gl c in let t2 = Tacmach.New.pf_concl gl 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) + Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Clenvtac.unify ~flags t1; + exact_no_check c] else exact_check c end -- cgit v1.2.3 From bae932cbd7ee0a5328a0913c09ae463b060f1f2f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:38:34 +0100 Subject: unsafe_type_of -> type_of in Eqdecide (2 occurrences) --- tactics/eqdecide.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'tactics') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bdfd200988..a82b26f428 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -195,13 +195,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with ] | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl a1 in + let sigma, rectype = pf_type_of gl a1 in let decide = mk rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in let subtacs = if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] else [diseqCase hyps eqonleft;eqCase tac;default_auto] in - (tclTHENS (elim_type decide) subtacs) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (elim_type decide) subtacs) end | _ -> invalid_arg "List.fold_right2" @@ -274,11 +274,12 @@ let compare c1 c2 = pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc -> pf_constr_of_global (lib_ref "core.not.type") >>= fun notc -> Proofview.Goal.enter begin fun gl -> - let rectype = pf_unsafe_type_of gl c1 in + let sigma, rectype = pf_type_of gl c1 in let ops = (opc,eqc,notc) in let decide = mkDecideEqGoal true ops rectype c1 c2 in - (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (onLastHyp simplest_case) clear_last)); - decideEquality rectype ops]) + tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (onLastHyp simplest_case) clear_last)); + decideEquality rectype ops]) end -- cgit v1.2.3 From 9655b3413544319e1bb6633744c67d6ddc303f1d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:39:59 +0100 Subject: unsafe_type_of -> type_of in Tactics.convert_concl --- tactics/tactics.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f6f7c71dfd..a44d83141e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -151,11 +151,12 @@ let convert_concl ~check ty k = Refine.refine ~typecheck:false begin fun sigma -> let sigma = if check then begin - ignore (Typing.unsafe_type_of env sigma ty); + let sigma, _ = Typing.type_of env sigma ty in match Reductionops.infer_conv env sigma ty conclty with | None -> error "Not convertible." | Some sigma -> sigma - end else sigma in + end else sigma + in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in (sigma, ans) -- cgit v1.2.3 From 3fcf06878d10a4a0c17d7095da964ebf15ed922b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:40:57 +0100 Subject: unsafe_type_of -> type_of in Tactics.change_on_subterm --- tactics/tactics.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a44d83141e..b0ee02a631 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -850,12 +850,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c = change_and_check Reduction.CONV mayneedglobalcheck true (t subst) else fun env sigma _c -> t subst env sigma) env sigma c in - if !mayneedglobalcheck then + let sigma = if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env sigma c) + try fst (Typing.type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." - end; + end else sigma + in (sigma, c) let change_in_concl ~check occl t = -- cgit v1.2.3 From 92d34ac2a926ebbe7a1cf339bd3cce0c529a99ec Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:50:17 +0100 Subject: unsafe_type_of + match -> sort_of in Tactics.cut --- tactics/tactics.ml | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b0ee02a631..6bd2041e3b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1310,30 +1310,23 @@ let cut c = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let relevance = - try - (* Backward compat: ensure that [c] is well-typed. Plus we - need to know the relevance *) - let typ = Typing.unsafe_type_of env sigma c in - let typ = whd_all env sigma typ in - match EConstr.kind sigma typ with - | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s)) - | _ -> None - with e when Pretype_errors.precatchable_exception e -> None - in - match relevance with - | Some r -> + (* Backward compat: ensure that [c] is well-typed. Plus we need to + know the relevance *) + match Typing.sort_of env sigma c with + | exception e when Pretype_errors.precatchable_exception e -> + Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + | sigma, s -> + let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in - Refine.refine ~typecheck:false begin fun h -> - let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in - let (h, x) = Evarutil.new_evar env h c in - let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - (h, f) - end - | None -> - Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun h -> + let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in + let (h, x) = Evarutil.new_evar env h c in + let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in + (h, f) + end) end let error_uninstantiated_metas t clenv = -- cgit v1.2.3 From f459030b71fb9bc18fe3b9e9f1c199c4ccd7db09 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:06:00 +0100 Subject: unsafe_type_of -> type_of in Tactics.find_eliminator --- tactics/tactics.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6bd2041e3b..d9f16a7a71 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1528,16 +1528,19 @@ exception IsNonrec let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite -let find_ind_eliminator ind s gl = - let env = Proofview.Goal.env gl in +let find_ind_eliminator env sigma ind s = let gr = lookup_eliminator env ind s in - Tacmach.New.pf_apply Evd.fresh_global gl gr + Evd.fresh_global env sigma gr let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + let ((ind,u),t) = reduce_to_quantified_ind env sigma t 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) } + let sigma, c = find_ind_eliminator env sigma ind (Retyping.get_sort_family_of env sigma concl) in + sigma, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -4774,7 +4777,9 @@ let elim_scheme_type elim t = let elim_type t = Proofview.Goal.enter begin fun gl -> let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in - let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in + let evd, elimc = Tacmach.New.pf_apply find_ind_eliminator gl (fst ind) + (Tacticals.New.elimination_sort_of_goal gl) + in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t) end -- cgit v1.2.3 From 2397d52d8e2f337ffd53d1198b21bb882b52d8a8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:09:56 +0100 Subject: unsafe_type_of -> type_of in Tactics.cut_and_apply --- tactics/tactics.ml | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d9f16a7a71..ca66f4bce2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1926,18 +1926,20 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta let cut_and_apply c = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - 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 - Refine.refine ~typecheck:false begin fun sigma -> - let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in - let (sigma, f) = Evarutil.new_evar env sigma typ in - let (sigma, x) = Evarutil.new_evar env sigma c1 in - (sigma, mkApp (f, [|mkApp (c, [|x|])|])) - end - | _ -> error "lapply needs a non-dependent product." + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let sigma, t = Typing.type_of env sigma c in + match EConstr.kind sigma (hnf_constr env sigma t) with + | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in + let (sigma, f) = Evarutil.new_evar env sigma typ in + let (sigma, x) = Evarutil.new_evar env sigma c1 in + (sigma, mkApp (f, [|mkApp (c, [|x|])|])) + end) + | _ -> error "lapply needs a non-dependent product." end (********************************************************************) -- cgit v1.2.3 From 38ec1c5ed4407348dc137d2c459edd0bebef7808 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:25:38 +0100 Subject: unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes) --- tactics/equality.ml | 23 ++++++++++++----------- tactics/hipattern.ml | 19 +++++++++---------- tactics/hipattern.mli | 4 ++-- tactics/tactics.ml | 16 +++++++++------- 4 files changed, 32 insertions(+), 30 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 96b61b6994..65f23ab0e4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1069,7 +1069,8 @@ let onEquality with_evars tac (c,lbindc) = 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 let eqn = clenv_type eq_clause' in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + (* FIXME evar leak *) + let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1341,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in - let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in let existTconstr = Coqlib.lib_ref "core.sigT.intro" in @@ -1603,7 +1604,7 @@ let cutSubstInConcl l2r eqn = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1620,7 +1621,7 @@ let cutSubstInHyp l2r eqn id = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in + let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in @@ -1715,7 +1716,7 @@ let is_eq_x gl x d = | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in - let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in + let (_,lhs,rhs) = pi3 (pf_apply 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)) with Constr_matching.PatternMatchingFailure -> @@ -1812,7 +1813,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let find_equations gl = let env = Proofview.Goal.env gl in let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in @@ -1837,7 +1838,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) @@ -1863,7 +1864,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let-ins *) Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in @@ -1887,19 +1888,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let cond_eq_term_left c t gl = try - let (_,x,_) = pi3 (find_eq_data_decompose gl t) in + let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try - let (_,_,x) = pi3 (find_eq_data_decompose gl t) in + let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try - let (_,x,y) = pi3 (find_eq_data_decompose gl t) in + let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 90a9a7acd9..1f68117a76 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -19,7 +19,6 @@ open Inductiveops open Constr_matching open Coqlib open Declarations -open Tacmach.New open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let hd,u = destInd sigma (fst (destApp sigma eqn)) in d,u,k -let extract_eq_args gl = function +let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (t,e1,e2) + let t = Typing.unsafe_type_of env sigma 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) + if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure -let find_eq_data_decompose gl eqn = - let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in - (lbeq,u,extract_eq_args gl eq_args) +let find_eq_data_decompose env sigma eqn = + let (lbeq,u,eq_args) = find_eq_data sigma eqn in + (lbeq,u,extract_eq_args env sigma eq_args) -let find_this_eq_data_decompose gl eqn = +let find_this_eq_data_decompose env sigma eqn = let (lbeq,u,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) - find_eq_data (project gl) eqn + find_eq_data sigma eqn with PatternMatchingFailure -> user_err (str "No primitive equality found.") in let eq_args = - try extract_eq_args gl eq_args + try extract_eq_args env sigma eq_args with PatternMatchingFailure -> user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 803305a1ca..0000f81d3f 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -122,11 +122,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca66f4bce2..3a4a2dc814 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2285,8 +2285,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented") let declare_intro_decomp_eq f = intro_decomp_eq_function := f -let my_find_eq_data_decompose gl t = - try Some (find_eq_data_decompose gl t) +let my_find_eq_data_decompose env sigma t = + try Some (find_eq_data_decompose env sigma t) with e when is_anomaly e (* Hack in case equality is not yet defined... one day, maybe, known equalities will be dynamically registered *) @@ -2296,13 +2296,15 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq ?loc l thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in - match my_find_eq_data_decompose gl t with + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let _,t = reduce_to_quantified_ind env sigma t in + match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) - (eq,t,eq_args) (c, t) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) + (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") end -- cgit v1.2.3 From c822b3de7f2a443cd920195fe94be1e7ceda3dbb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:31:44 +0100 Subject: unsafe_type_of -> type_of in Tactics.intro_or_and_pattern --- tactics/tactics.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a4a2dc814..e859055d4a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2312,16 +2312,19 @@ let intro_decomp_eq ?loc l thin tac id = let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let (ind,t) = reduce_to_quantified_ind env sigma t in let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in - Tacticals.New.tclTHENLASTn - (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) - (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) - nv_with_let ll) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHENLASTn + (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) + (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) + nv_with_let ll)) end let rewrite_hyp_then assert_style with_evars thin l2r id tac = -- cgit v1.2.3 From e12cfbafbce3a1c6719d7e4d34fe64a81cce90b2 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:35:26 +0100 Subject: unsafe_type_of -> type_of in Tactics.rewrite_hyp_then (+ tclEVARSTHEN) --- tactics/tactics.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e859055d4a..87389f0be0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -47,6 +47,9 @@ open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +let tclEVARS = Proofview.Unsafe.tclEVARS +let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t + let inj_with_occurrences e = (AllOccurrences,e) let typ_of env sigma c = @@ -2338,9 +2341,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in 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 (type_of (mkVar id)) in + let sigma, t = Typing.type_of env sigma (mkVar id) in + let t = whd_all env sigma t in let eqtac, thin = match match_with_equality_type env sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then @@ -2366,7 +2368,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin in (* Skip the side conditions of the rewriting step *) - Tacticals.New.tclTHENFIRST eqtac (tac thin) + tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end let prepare_naming ?loc = function -- cgit v1.2.3 From 3faf22b382379f08d5a918bd535287f57e2fc0fc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:39:49 +0100 Subject: unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_then Not 100% sure about this one TBH, this function is messy. --- tactics/tactics.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 87389f0be0..da798dd2ce 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3399,8 +3399,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match EConstr.kind sigma c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar env sigma (type_of c) Anonymous in + let type_of = Tacmach.New.pf_get_type_of gl in + id_of_name_using_hdchar env sigma (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) -- cgit v1.2.3 From dd4c9f7218f3d4fd883c0ae73cd41cd12049e86e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:46:15 +0100 Subject: unsafe_type_of -> type_of in Tactics.abstract_args --- tactics/tactics.ml | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index da798dd2ce..f5685e07af 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3802,15 +3802,15 @@ let is_defined_variable env id = env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = - let open Tacmach.New in let open Context.Rel.Declaration in let sigma = ref (Tacmach.New.project gl) in let env = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in + let hyps = Proofview.Goal.hyps gl in let dep = dep || local_occur_var !sigma id concl in let avoid = ref Id.Set.empty in let get_id name = - let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in + let id = fresh_id_in_env !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") env in avoid := Id.Set.add id !avoid; id in (* Build application generalized w.r.t. the argument plus the necessary eqs. @@ -3819,14 +3819,14 @@ let abstract_args gl generalize_vars dep id defined f args = eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *) *) - let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = + let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars) arg = let name, ty_relevance, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c in - let argty = Tacmach.New.pf_unsafe_type_of gl arg in - let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let sigma', argty = Typing.type_of env !sigma arg in + let sigma', ty = Evarsolve.refresh_universes (Some true) env sigma' ty in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3834,7 +3834,7 @@ let abstract_args gl generalize_vars dep id defined f args = match EConstr.kind !sigma arg with | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) -> (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, - Id.Set.add id nongenvars, Id.Set.remove id vars, env) + Id.Set.add id nongenvars, Id.Set.remove id vars) | _ -> let name = get_id name in let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in @@ -3856,7 +3856,7 @@ let abstract_args gl generalize_vars dep id defined f args = let refls = refl :: refls in let argvars = ids_of_constr !sigma vars arg in (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, - nongenvars, Id.Set.union argvars vars, env) + nongenvars, Id.Set.union argvars vars) in let f', args' = decompose_indapp !sigma f args in let dogen, f', args' = @@ -3870,15 +3870,16 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let tyf' = Tacmach.New.pf_unsafe_type_of gl f' 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' + let sigma', tyf' = Typing.type_of env !sigma f' in + sigma := sigma'; + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars = + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty) args' in let args, refls = List.rev args, List.rev refls in let vars = if generalize_vars then let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars + hyps_of_vars env !sigma hyps nogen vars else [] in let body, c' = @@ -3886,7 +3887,7 @@ let abstract_args gl generalize_vars dep id defined f args = else None, c' in let typ = Tacmach.New.pf_get_hyp_typ id gl in - let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in + let tac = make_abstract_generalize env 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) else None -- cgit v1.2.3 From 8a736c4d3aaf941416ffc616c296a3b077d6242f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:48:14 +0100 Subject: unsafe_type_of -> type_of in Tactics.guess_elim --- tactics/tactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f5685e07af..1624c4a62d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4231,8 +4231,8 @@ let guess_elim isrec dep s hyp0 gl = let ind = EConstr.of_constr ind in (sigma, ind) in - let elimt = Typing.unsafe_type_of env sigma elimc in - sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) + let sigma, elimt = Typing.type_of env sigma elimc in + sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in -- cgit v1.2.3 From 9268c5f9e066730eef6f831b4fcdc55f5a022b36 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:49:00 +0100 Subject: unsafe_type_of -> type_of in Tactics.given_elim --- tactics/tactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1624c4a62d..046d76294c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4238,8 +4238,8 @@ 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 ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in - let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - Tacmach.New.project gl, (e, elimt), ind_type_guess + let sigma, elimt = Tacmach.New.pf_type_of gl elimc in + sigma, (e, elimt), ind_type_guess type scheme_signature = (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array -- cgit v1.2.3 From a9e4f78935ba091d7e012df8398bccc5d08d1370 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:51:18 +0100 Subject: Fix evar map leak in Tactics.find_induction_type --- tactics/tactics.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 046d76294c..14d8e4fccd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4249,26 +4249,25 @@ type eliminator_source = | ElimOver of bool * Id.t let find_induction_type isrec elim hyp0 gl = - let sigma = Tacmach.New.project gl in - let scheme,elim = + let sigma, scheme,elim = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in let scheme = compute_elim_sig sigma ~elimc elimt in (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + sigma, scheme, ElimOver (isrec,hyp0) | Some e -> - let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in + let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in + let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in - scheme, ElimUsing (elim,indsign) + sigma, scheme, ElimUsing (elim,indsign) in match scheme.indref with | None -> error_ind_scheme "" - | Some ref -> ref, scheme.nparams, elim + | Some ref -> sigma, (ref, scheme.nparams, elim) let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 @@ -4389,10 +4388,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 gl in - atomize_param_of_ind_then elim_info hyp0 (fun indvars -> - apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names - (fun elim -> induction_tac with_evars [] [hyp0] elim)) + let sigma, elim_info = find_induction_type isrec elim hyp0 gl in + tclEVARSTHEN sigma + (atomize_param_of_ind_then elim_info hyp0 (fun indvars -> + apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names + (fun elim -> induction_tac with_evars [] [hyp0] elim))) end let msg_not_right_number_induction_arguments scheme = -- cgit v1.2.3 From 276aa928c9b3c2337aebf21383e18f145735426b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:55:29 +0100 Subject: unsafe_type_of -> get_type_of in Tactics.is_functional_induction --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 14d8e4fccd..6ed6e49b7e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4274,7 +4274,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 (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in + let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_get_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 -- cgit v1.2.3 From 5251ffebaa19fa22866ccd537b8d7cfe6aaadf5c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 15:58:43 +0100 Subject: unsafe_type_of -> type_of in Tactics.induction_gen_l + fix bad env --- tactics/tactics.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ed6e49b7e..8f7fbe7552 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4667,18 +4667,16 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_unsafe_type_of gl in - let sigma = Tacmach.New.project gl in - Proofview.tclENV >>= fun env -> - let x = - id_of_name_using_hdchar env sigma (type_of c) Anonymous in - + let sigma, t = pf_apply Typing.type_of gl c in + let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in let id = new_fresh_id Id.Set.empty x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let () = newlc:=id::!newlc in - Tacticals.New.tclTHEN - (letin_tac None (Name id) c None allHypsAndConcl) - (atomize_list newl') + Tacticals.New.tclTHENLIST [ + tclEVARS sigma; + letin_tac None (Name id) c None allHypsAndConcl; + atomize_list newl'; + ] end in Tacticals.New.tclTHENLIST [ -- cgit v1.2.3 From 6f72abed5c2342491830590c66f00f0a68be81d9 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:01:02 +0100 Subject: unsafe_type_of -> type_of in Tactics.symmetry_in I'm a bit dubious about the tclENV in match_with_equation but let's leave it for now. --- tactics/tactics.ml | 47 +++++++++++++++++++++++------------------------ 1 file changed, 23 insertions(+), 24 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8f7fbe7552..a53191a579 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4866,7 +4866,8 @@ let prove_symmetry hdcncl eq_kind = Tacticals.New.onLastHyp simplest_case; one_constructor 1 NoBindings ]) -let match_with_equation sigma c = +let match_with_equation c = + Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> try let res = match_with_equation env sigma c in @@ -4879,9 +4880,8 @@ let symmetry_red allowred = (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from 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 - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN @@ -4903,25 +4903,25 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in - let sign,t = decompose_prod_assum sigma ctype in - Proofview.tclORELSE - begin - match_with_equation sigma t >>= fun (_,hdcncl,eq) -> - let symccl = - match eq with - | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) - | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in - Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) - [ intro_replacing id; - Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] - end - begin function (e, info) -> match e with - | NoEquationFound -> Hook.get forward_setoid_symmetry_in id - | e -> Proofview.tclZERO ~info e - end + let sigma, ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let sign,t = decompose_prod_assum sigma ctype in + tclEVARSTHEN sigma + (Proofview.tclORELSE + begin + match_with_equation t >>= fun (_,hdcncl,eq) -> + let symccl = + match eq with + | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) + | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in + Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + end + begin function (e, info) -> match e with + | NoEquationFound -> Hook.get forward_setoid_symmetry_in id + | e -> Proofview.tclZERO ~info e + end) end let intros_symmetry = @@ -4974,9 +4974,8 @@ let transitivity_red allowred t = (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from 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 - match_with_equation sigma concl >>= fun with_eqn -> + match_with_equation concl >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN -- cgit v1.2.3 From eb9fb89e9170e3fcab668c638351faa037b92756 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:03:14 +0100 Subject: unsafe_type_of -> type_of in Tactics.prove_transitivity --- tactics/tactics.ml | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a53191a579..827f44ec1e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4948,25 +4948,26 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = Proofview.Goal.enter begin fun gl -> - let (eq1,eq2) = match eq_kind with - | MonomorphicLeibnizEq (c1,c2) -> - mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) - | PolymorphicLeibnizEq (typ,c1,c2) -> - mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) - | HeterogenousEq (typ1,c1,typ2,c2) -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let type_of = Typing.unsafe_type_of env sigma in - let typt = type_of t in - (mkApp(hdcncl, [| typ1; c1; typt ;t |]), - mkApp(hdcncl, [| typt; t; typ2; c2 |])) - in - Tacticals.New.tclTHENFIRST (cut eq2) - (Tacticals.New.tclTHENFIRST (cut eq1) - (Tacticals.New.tclTHENLIST - [ Tacticals.New.tclDO 2 intro; - Tacticals.New.onLastHyp simplest_case; - assumption ])) + let sigma = Tacmach.New.project gl in + let sigma, eq1, eq2 = match eq_kind with + | MonomorphicLeibnizEq (c1,c2) -> + sigma, mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) + | PolymorphicLeibnizEq (typ,c1,c2) -> + sigma, mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) + | HeterogenousEq (typ1,c1,typ2,c2) -> + let env = Proofview.Goal.env gl in + let sigma, typt = Typing.type_of env sigma t in + sigma, + mkApp(hdcncl, [| typ1; c1; typt ;t |]), + mkApp(hdcncl, [| typt; t; typ2; c2 |]) + in + tclEVARSTHEN sigma + (Tacticals.New.tclTHENFIRST (cut eq2) + (Tacticals.New.tclTHENFIRST (cut eq1) + (Tacticals.New.tclTHENLIST + [ Tacticals.New.tclDO 2 intro; + Tacticals.New.onLastHyp simplest_case; + assumption ]))) end let transitivity_red allowred t = -- cgit v1.2.3 From 34d95672ecace6733d9d2f738ee6d7aee46fb2d0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:06:03 +0100 Subject: unsafe_type_of -> get_type_of in Hints.make_trivial --- tactics/hints.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'tactics') diff --git a/tactics/hints.ml b/tactics/hints.ml index 7b3797119a..73e8331bcb 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -26,7 +26,6 @@ open Libnames open Smartlocate open Termops open Inductiveops -open Typing open Typeclasses open Pattern open Patternops @@ -966,16 +965,17 @@ 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 (unsafe_type_of env sigma c) in + let t = hnf_constr env sigma (Retyping.get_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; - poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); - name = name; - db = None; - secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + (Some hd, + { pri=1; + poly = poly; + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); + name = name; + db = None; + secvars = secvars_of_constr env sigma c; + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) -- cgit v1.2.3 From d584d0643e32f2277b1a38ba46fc92993638492b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:07:00 +0100 Subject: unsafe_type_of -> get_type_of in Hipattern.extract_eq_args --- tactics/hipattern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 1f68117a76..c5ed02e043 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -453,7 +453,7 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = Typing.unsafe_type_of env sigma e1 in (t,e1,e2) + let t = Retyping.get_type_of env sigma e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) -- cgit v1.2.3 From 1fd5cec8fbc7323ac7bd710707f37d906c5bc794 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:10:21 +0100 Subject: unsafe_type_of -> get_type_of in Tacticals.general_elim_then_using --- tactics/tacticals.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ed7ab9164a..5db72e669e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -633,7 +633,7 @@ module New = struct (Proofview.Goal.enter begin fun gl -> let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv -- cgit v1.2.3 From 598558339afec652467c78d0bd6e472df051ef69 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:11:41 +0100 Subject: unsafe_type_of -> get_type_of in Tacticals.elimination_then --- tactics/tacticals.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5db72e669e..199fdd50c4 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -741,7 +741,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | NotRecord -> true,gl_make_elim -- cgit v1.2.3 From 5a2600f47b64495a8754be74f3156f915a2497ec Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:13:32 +0100 Subject: unsafe_type_of -> get_type_of in Class_tactics.autoapply --- tactics/class_tactics.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f8cb8870ea..ccd88d2c35 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,10 +1202,9 @@ let autoapply c i = in let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in - let cty = Tacmach.New.pf_unsafe_type_of gl c in + let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - unify_e_resolve false flags gl - ((c,cty,Univ.ContextSet.empty),0,ce) <*> + unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in -- cgit v1.2.3 From 50f5b99e9ffce8d7a54b1a35b899e0645df72632 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:15:53 +0100 Subject: unsafe_type_of -> get_type_of in Contradiction.contradiction_term --- tactics/contradiction.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 1f5a6380fd..c7b6998c8c 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in 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 = Tacmach.New.pf_get_type_of gl c in let _, ccl = splay_prod env sigma typ in if is_empty_type env sigma ccl then Tacticals.New.tclTHEN -- cgit v1.2.3 From 907df42d15904c13b4e8c5af0e24ff0406b3f6ed Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:29:29 +0100 Subject: unsafe_type_of -> get_type_of in Autorewrite.{find,decompose}_applied_relation --- tactics/autorewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index cd6f445503..1bbcca8827 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = in try let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) let open EConstr in let hyp_ty = Unsafe.to_constr ty in @@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation ?loc metas env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in + let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> -- cgit v1.2.3 From 42c28946cded7e81ade816416fc1538341fd4da8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:37:33 +0100 Subject: unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply in ifOnHyp --- tactics/elim.ml | 7 ++----- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- 3 files changed, 4 insertions(+), 7 deletions(-) (limited to 'tactics') diff --git a/tactics/elim.ml b/tactics/elim.ml index ea61b8e4df..c0d533a6f2 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_unsafe_type_of gl in - let env = pf_env gl in - let sigma = project gl in - let typc = type_of c in + let typc = pf_get_type_of gl c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) + (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); exact_no_check c ] end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 199fdd50c4..58d2097dea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -587,7 +587,7 @@ module New = struct let ifOnHyp pred tac1 tac2 id = Proofview.Goal.enter begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in - if pred (id,typ) then + if pf_apply pred gl (id,typ) then tac1 id else tac2 id diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 31d26834d6..4b93b81d1c 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -222,7 +222,7 @@ module New : sig val nLastDecls : Proofview.Goal.t -> int -> named_context - val ifOnHyp : (Id.t * types -> bool) -> + val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) -> (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> Id.t -> unit Proofview.tactic -- cgit v1.2.3 From 63883d37318fa54101b3ec4029cb26f0ae8439a3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:39:06 +0100 Subject: unsafe_type_of -> get_type_of in Elim.induction_trailer --- tactics/elim.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/elim.ml b/tactics/elim.ml index c0d533a6f2..379a8d5401 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.enter begin fun gl -> - let idty = pf_unsafe_type_of gl (mkVar id) in + let idty = pf_get_type_of gl (mkVar id) 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 -- cgit v1.2.3 From 1c1eed73491ea84ee58eec703fbeedf9667a06ef Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 16:40:15 +0100 Subject: unsafe_type_of -> get_type_of in Inv.raw_inversion --- tactics/inv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/inv.ml b/tactics/inv.ml index be0421d42d..2181eb25af 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -464,7 +464,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 (pf_unsafe_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg -- cgit v1.2.3 From b1d6846e31cd43b850feb30fe15acb9d27fb96e4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:06:18 +0100 Subject: unsafe_type_of -> (get_)type_of in Equality.{discrEq,minimal_free_rels_rec,sig_clausal_form} --- tactics/equality.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 65f23ab0e4..1e1673e478 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1062,9 +1062,8 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.enter begin fun gl -> - 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 = pf_get_type_of gl c 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 @@ -1166,7 +1165,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, unsafe_type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_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 @@ -1211,7 +1210,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = unsafe_type_of env sigma dflt in + let sigma, dflt_typ = type_of env sigma dflt in try let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in -- cgit v1.2.3 From c38e60243a3cee5d23c76fd78362b7c352c3d8ca Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:07:00 +0100 Subject: Remove useless unification in Equality.sig_clausal_form We unify [w_type = type of w] with [a], but [w] was created with type [a]. This code was introduced in eab11e537905472fdcc3257bc9913df82c82b3e4 to fix #2255, AFAICT only the [minimal_free_rels_rec] part is necessary. --- tactics/equality.ml | 32 ++++++++++++-------------------- 1 file changed, 12 insertions(+), 20 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 1e1673e478..0eb0a30486 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1224,29 +1224,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in - let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in - match evopt with - | Some w -> - let w_type = unsafe_type_of env sigma w in - begin match Evarconv.unify_leq_delay env sigma w_type a with - | sigma -> - let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in - sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - | exception Evarconv.UnableToUnify _ -> - user_err Pp.(str "Cannot solve a unification problem.") - end - | None -> - (* This at least happens if what has been detected as a - dependency is not one; use an evasive error message; - even if the problem is upwards: unification should be - tried in the first place in make_iterated_tuple instead - of approximatively computing the free rels; then - unsolved evars would mean not binding rel *) - user_err Pp.(str "Cannot solve a unification problem.") + if EConstr.isEvar sigma ev then + (* This at least happens if what has been detected as a + dependency is not one; use an evasive error message; + even if the problem is upwards: unification should be + tried in the first place in make_iterated_tuple instead + of approximatively computing the free rels; then + unsolved evars would mean not binding rel *) + user_err Pp.(str "Cannot solve a unification problem.") + else + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail]) in let sigma = Evd.clear_metas sigma in let sigma, scf = sigrec_clausal_form sigma siglen ty in - sigma, Evarutil.nf_evar sigma scf + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors -- cgit v1.2.3 From 53cabaf1e26bfc13e5a45dfeb90ad6a858344c32 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:11:07 +0100 Subject: unsafe_type_of -> get_type_of in Equality.build_injrec --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 0eb0a30486..de7e755e5a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1311,7 +1311,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,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in -- cgit v1.2.3 From 8a8217fe0b1ba8b7548ae648368774105cf21b11 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:12:07 +0100 Subject: unsafe_type_of -> get_type_of in Equality.inject_if_homogenous_dependent_pair --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index de7e755e5a..9195746dc6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1352,7 +1352,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) -- cgit v1.2.3 From 38e1e823cf5329762e97902a6ded54c95a5a5c61 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:13:33 +0100 Subject: unsafe_type_of -> get_type_of in Leminv.lemInv --- tactics/leminv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/leminv.ml b/tactics/leminv.ml index cf58c9306c..def4af1ae8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let lemInv id c = Proofview.Goal.enter begin fun gls -> try - let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in + let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with -- cgit v1.2.3 From 48b142d0e915e946274c14ab354f174cc5b6df51 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:41:49 +0100 Subject: Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of) --- tactics/tactics.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 827f44ec1e..609b752716 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4772,7 +4772,10 @@ let destruct ev clr c l e = let elim_scheme_type elim t = Proofview.Goal.enter begin fun gl -> - let clause = mk_clenv_type_of gl elim in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, elimt = Typing.type_of env sigma elim in + let clause = mk_clenv_from_env env sigma None (elim,elimt) in match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> let clause' = -- cgit v1.2.3 From af788fd0daeed459b98ed9acd3a0443f53666176 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 17:52:29 +0100 Subject: unsafe_type_of -> type_of in Sequent.extend_with_auto_hints + fix evar leak in caller --- tactics/hints.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'tactics') diff --git a/tactics/hints.mli b/tactics/hints.mli index 2a9b71387e..9c9f0b7708 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -160,6 +160,8 @@ module Hint_db : val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit + val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a + val use_dn : t -> bool val transparent_state : t -> TransparentState.t val set_transparent_state : t -> TransparentState.t -> t -- cgit v1.2.3