From 04a8c766a51b17997d8a9ffcf6f2d7beffc599ce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Apr 2020 15:35:40 +0200 Subject: Remove a critical call to V82.tactic in Clenvtac. Despite being marked as a breaking change by myself, it seems that the underlying condition had been solved in the meantime. --- proofs/clenvtac.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 767f93787d..197d69a481 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -61,10 +61,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv = clenv_pose_metas_as_evars clenv dep_mvs let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - (* ppedrot: a Goal.enter here breaks things, because the tactic below may - solve goals by side effects, while the compatibility layer keeps those - useless goals. That deserves a FIXME. *) - Proofview.V82.tactic begin fun gl -> + Proofview.Goal.enter begin fun gl -> let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then @@ -78,9 +75,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = else clenv.evd in let clenv = { clenv with evd = evd' } in - tclTHEN - (tclEVARS (Evd.clear_metas evd')) - (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) + (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))) end let clenv_pose_dependent_evars ?(with_evars=false) clenv = -- cgit v1.2.3 From 1109581ba7afca804515fc6179565da808bae4f7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Apr 2020 15:57:54 +0200 Subject: Wrap Refiner.refiner in the tactic monad. This function was used almost everywhere with the wrapper around. --- proofs/clenvtac.ml | 2 +- proofs/refiner.ml | 2 ++ proofs/refiner.mli | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 197d69a481..695e103082 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -77,7 +77,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) - (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) end let clenv_pose_dependent_evars ?(with_evars=false) clenv = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 75c3436cf4..6a0ba30bbf 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -37,6 +37,8 @@ let refiner ~check = CProfile.profile2 refiner_key (refiner ~check) else refiner ~check +let refiner ~check c = Proofview.V82.tactic (refiner ~check c) + (*********************) (* Tacticals *) (*********************) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 66eae1db81..d4f2239a59 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -22,7 +22,7 @@ val project : 'a sigma -> evar_map val pf_env : Goal.goal sigma -> Environ.env val pf_hyps : Goal.goal sigma -> named_context -val refiner : check:bool -> Constr.t -> tactic +val refiner : check:bool -> Constr.t -> unit Proofview.tactic (** {6 Tacticals. } *) -- cgit v1.2.3 From 6839a2c9b7d2480e21572a7d176dcd6ea0617159 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Apr 2020 16:05:19 +0200 Subject: Remove a very specific low-level tactical from Refiner. It was only used at one point in the STM, and its localization was suprising to say the least. Furthermore it was relying on legacy code. Instead we hardcode it in the STM. --- proofs/refiner.ml | 2 -- proofs/refiner.mli | 1 - 2 files changed, 3 deletions(-) (limited to 'proofs') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6a0ba30bbf..ad84afd47e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -271,5 +271,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = - tclEVARS (Evd.merge_universe_context (project gl) ctx) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d4f2239a59..3471f38e9e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies -- cgit v1.2.3 From d87f8d10d089c3a33ddb36a71ab6fc082d0d1140 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2020 09:00:49 +0200 Subject: Fix GeoCoq slowdown. There is no point in normalizing the goal in the legacy refiner because the function is actually insensitive to evars. --- proofs/refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ad84afd47e..29a47c5acd 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -37,7 +37,7 @@ let refiner ~check = CProfile.profile2 refiner_key (refiner ~check) else refiner ~check -let refiner ~check c = Proofview.V82.tactic (refiner ~check c) +let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c) (*********************) (* Tacticals *) -- cgit v1.2.3