diff options
| author | Hugo Herbelin | 2015-02-19 15:00:57 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-19 15:00:57 +0100 |
| commit | b898ccc8660215ce80a280e51741eacae8a7525c (patch) | |
| tree | 4ae767e840ca90d9cfc3dcea4e2bbb62fa12796e | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
When looking for restrictions in ?n=?p problems, keep the type of let-bindings.
Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that
occur-check is done in [T] as well as in [M] (except when [M] is a
variable, where it is hopefully not necessary).
This is a way to fix #4062 (evars with type depending on themselves).
The fix modifies the alias map (make_alias_map) but it should behave
the same at all places using alias maps other than
has_constrainable_free_vars.
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index adfe9dd8de..c894f5717e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -217,7 +217,7 @@ let compute_var_aliases sign = sign Id.Map.empty let compute_rel_aliases var_aliases rels = - snd (List.fold_right (fun (_,b,t) (n,aliases) -> + snd (List.fold_right (fun (_,b,u) (n,aliases) -> (n-1, match b with | Some t -> @@ -231,7 +231,7 @@ let compute_rel_aliases var_aliases rels = try Int.Map.find (p+n) aliases with Not_found -> [] in Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases | _ -> - Int.Map.add n [lift n t] aliases) + Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases) | None -> aliases)) rels (List.length rels,Int.Map.empty)) |