diff options
| author | Hugo Herbelin | 2014-11-03 20:20:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-04 16:34:12 +0100 |
| commit | bcba6d1bc9f769da593a3b01a12846f3e7a26a25 (patch) | |
| tree | f09be5662a73315b38a21f49afc0dd8b8407cf4b /pretyping/evd.mli | |
| parent | d1321c8d686cc0e392c8ae26beb8abe762258900 (diff) | |
Experimentally applying eager evar substitution at the same time as
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 54c5d9bf23..513ade646b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -443,7 +443,7 @@ 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 : metabinding list -> constr -> constr option +val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option (** {5 FIXME: Nothing to do here} *) |