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 /engine/evd.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 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 993ed300b..5619b7af2 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -601,10 +601,6 @@ val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - type open_constr = evar_map * constr (* Special case when before is empty *) (** Partially constructed constrs. *) |