From 57ef36dbdcfe2f5bc47dc1e9dbb1785010d2c151 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 19:31:21 +0200 Subject: Remove a useless use of clenv_fchain in Equality. The clenv was generated to eliminate a negation, but its argument was given immediately and its type statically known to be the same. --- tactics/equality.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 535725b11d..7a3467cace 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1049,9 +1049,8 @@ let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow (clenv_type eq_clause) Sorts.Relevant false_0 in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenv.clenv_value_cast_meta absurd_clause in + (* pf : eq t t1 t2 -> False *) + let pf = EConstr.mkApp (pf, [|clenv_value eq_clause|]) in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -- cgit v1.2.3 From c50d7aa6537b46aa0b791cdb28f9dbe66327e6ef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Sep 2020 12:00:42 +0200 Subject: Inline the last use of apply_on_clause in Equality. --- tactics/equality.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7a3467cace..88622d153c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1022,15 +1022,6 @@ type equality = { let eq_baseid = Id.of_string "e" -let apply_on_clause (f,t) clause = - let sigma = clause.evd in - let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in - let argmv = - (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> user_err (str "Ill-formed clause applicator.")) in - clenv_fchain ~with_univs:false argmv f_clause clause - let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> @@ -1405,7 +1396,15 @@ let inject_at_positions env sigma l2r eq posns tac = let sigma,congr = Evd.fresh_global env sigma eq.congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in - let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in + let inj_clause = + let sigma = eq_clause.evd in + let f_clause = mk_clenv_from_env eq_clause.env sigma None (pf, pf_typ) in + let argmv = + (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> user_err (str "Ill-formed clause applicator.")) in + clenv_fchain ~with_univs:false argmv f_clause eq_clause + in let pf = Clenv.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in evdref := sigma; -- cgit v1.2.3 From 31a9ad12f02c50c04dc9d125863a550f70f84dbb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Sep 2020 17:40:28 +0200 Subject: Remove the last use of clenv_fchain in Equality. Once again, we now statically the type of the argument is the same, so there is no need to call the old unification. --- tactics/equality.ml | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 88622d153c..26ae35a79d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1394,19 +1394,12 @@ let inject_at_positions env sigma l2r eq posns tac = let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda (make_annot e Sorts.Relevant) t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in - let pf = applist(congr,[t;resty;injfun;t1;t2]) in + (* pf : eq t t1 t2 -> eq resty (injfun t1) (injfun t2) *) + let pf = mkApp (congr,[|t; resty; injfun; t1; t2|]) in let sigma, pf_typ = Typing.type_of env sigma pf in - let inj_clause = - let sigma = eq_clause.evd in - let f_clause = mk_clenv_from_env eq_clause.env sigma None (pf, pf_typ) in - let argmv = - (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> user_err (str "Ill-formed clause applicator.")) in - clenv_fchain ~with_univs:false argmv f_clause eq_clause - in - let pf = Clenv.clenv_value_cast_meta inj_clause in - let ty = simplify_args env sigma (clenv_type inj_clause) in + let pf_typ = Vars.subst1 mkProp (pi3 @@ destProd sigma pf_typ) in + let pf = mkApp (pf, [| Clenv.clenv_value eq_clause |]) in + let ty = simplify_args env sigma pf_typ in evdref := sigma; Some (pf, ty) with Failure _ -> None -- cgit v1.2.3 From be494f51ec316f0e0af424d3febc1bd100112040 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Sep 2020 09:48:07 +0200 Subject: Remove a unused function from the Clenv API. --- proofs/clenv.ml | 3 --- proofs/clenv.mli | 1 - 2 files changed, 4 deletions(-) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 8e3cab70ea..4893758ab3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -618,9 +618,6 @@ let clenv_cast_meta clenv = in crec -let clenv_value_cast_meta clenv = - clenv_cast_meta clenv (clenv_value clenv) - let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 43e808dac7..d4905de434 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -99,7 +99,6 @@ val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv -val clenv_value_cast_meta : clausenv -> constr (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.t -- cgit v1.2.3