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.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'proofs/refine.ml') diff --git a/proofs/refine.ml b/proofs/refine.ml index e3f650848..90276951b 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -70,7 +70,6 @@ let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects let generic_refine ~typecheck f gl = - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in @@ -159,7 +158,6 @@ let with_type env evd c t = evd , j'.Environ.uj_val let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let f h = -- cgit v1.2.3