aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-22 19:06:54 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-23 11:54:48 +0100
commit8cfe40dbc02156228a529c01190c50d825495013 (patch)
treef40da159fed52eb9db479180bd323d59ba9245df /engine/evd.ml
parent8b73fd7c6ce423f8c8a2594e90200f2407795d52 (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.ml')
-rw-r--r--engine/evd.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 62d396395..b7d56a698 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1157,10 +1157,6 @@ let set_extra_data extras evd = { evd with extras }
(*******************************************************************)
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
type open_constr = evar_map * constr
(*******************************************************************)