diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-25 13:55:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-27 13:18:55 +0200 |
| commit | dca961d870a98e9e1eaab14850c2b0e2854a82f8 (patch) | |
| tree | 5afb8d895d530d2fedef2858d9552dd6d73d47dc /proofs/goal.mli | |
| parent | 38fbd7ca90ce3b852fa19b9706a00e64c5d73046 (diff) | |
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.
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 5 |
1 files changed, 0 insertions, 5 deletions
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 |