From 68935660fbfdec2e357e123ed999073ed3b8fc26 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Feb 2018 16:00:04 +0100 Subject: [engine] Remove ghost parameter from `Proofview.Goal.t` In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code. --- proofs/refine.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/refine.mli') diff --git a/proofs/refine.mli b/proofs/refine.mli index cfdcde36e..1932a306c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -33,7 +33,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr (** A variant of [refine] which assumes exactly one goal under focus *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> - [ `NF ] Proofview.Goal.t -> 'a tactic + Proofview.Goal.t -> 'a tactic (** The general version of refine. *) (** {7 Helper functions} *) -- cgit v1.2.3