From dca961d870a98e9e1eaab14850c2b0e2854a82f8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 25 Sep 2014 13:55:40 +0200 Subject: Removing the last use of tclSENSITIVE in favour of tclNEWGOALS. Most of the code from Goal.Refine and related was moved to the one file that was using it, wiz. tactics.ml. Some additional care should be taken to clean up even more the remaining code. --- proofs/goal.mli | 5 ----- 1 file changed, 5 deletions(-) (limited to 'proofs/goal.mli') diff --git a/proofs/goal.mli b/proofs/goal.mli index 4b85ec20b..4d4d0c2eb 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -120,9 +120,6 @@ end (*** Goal tactics. DEPRECATED. ***) -(* Goal tactics are [subgoal sensitive]-s *) -type subgoals = private { subgoals: goal list } - (* Goal sensitive values *) type +'a sensitive @@ -131,8 +128,6 @@ val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map -val refine_open_constr : Evd.open_constr -> subgoals sensitive - (* [enter] combines [env], [defs], [hyps] and [concl] in a single primitive. *) val enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive -- cgit v1.2.3