diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-22 19:06:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 11:54:48 +0100 |
| commit | 8cfe40dbc02156228a529c01190c50d825495013 (patch) | |
| tree | f40da159fed52eb9db479180bd323d59ba9245df /tactics/tactics.mli | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff) | |
Ensuring static invariants about handling of pending evars in Pretyping.
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7acfb6286..354ac50b4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option -> (** Common entry point for user-level "set", "pose" and "remember" *) val letin_pat_tac : (bool * intro_pattern_naming) option -> - Name.t -> pending_constr -> clause -> unit Proofview.tactic + Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic (** {6 Generalize tactics. } *) |