diff options
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 |