diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 14:07:43 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 14:46:37 +0100 |
| commit | d98fdf1ef5789f6d5420e52c34a33debf08584e9 (patch) | |
| tree | b61a0b679df7b56ff6180924395fa5671d4c9b8f /proofs/goal.mli | |
| parent | 4d6b938e90ecd9dbfb29a0af28a7d8b6a657ae17 (diff) | |
Code refactoring thanks to the new Monad module.
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index db864b273..87793878c 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -157,19 +157,6 @@ val defs : Evd.evar_map sensitive primitive. *) val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive -(*** Additional functions ***) - -(* emulates List.map for functions of type - [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating - new evar_map to next definition *) -val list_map : - (Evd.evar_map -> 'a -> 'b * Evd.evar_map) -> - 'a list -> Evd.evar_map -> - 'b list * Evd.evar_map - -(* emulates List.map for [sensitive] Kleisli functions. *) -val sensitive_list_map : ('a -> 'b sensitive) -> 'a list -> 'b list sensitive - (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) |