diff options
| author | Pierre-Marie Pédrot | 2015-09-27 16:36:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-27 16:47:30 +0200 |
| commit | 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 (patch) | |
| tree | fb4a962f5776a90c74ec14eb40175c95eb6604fc /engine/evd.mli | |
| parent | ca14b0bb67c9db000736333a056fc147c6f5199c (diff) | |
Removing subst_defined_metas_evars from Evd.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 0902191818..cfe4adc09d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -457,7 +457,6 @@ val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status val retract_coercible_metas : evar_map -> metabinding list * evar_map -val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option (** {5 FIXME: Nothing to do here} *) |