diff options
| author | Matthieu Sozeau | 2014-06-19 12:43:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-19 12:44:52 +0200 |
| commit | 2a8e86e504e57d3c47d65fee408cec9aa9419445 (patch) | |
| tree | 7347d260cdbd398171c92abfa2b9125cacc852df /pretyping | |
| parent | 83c17d79c3388ebd488559dcf99d5d019e60bb1c (diff) | |
- Fix bug in unification, not only named metas are turned into evars (e.g. in Ssreflect).
- Fix is_applied_rewrite_relation to look for propositional relations.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 236dc98765..58296002f9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -126,7 +126,7 @@ let rec subst_meta_instances bl c = let evar_source_of_meta mv evd = match Evd.meta_name evd mv with - | Anonymous -> assert false (* only dependent metas posed as evars (?) *) + | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) let pose_all_metas_as_evars env evd t = |