diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:05:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:05:00 +0200 |
| commit | 83ae5e6ad95372912ba9eb9f8c52d857cdf10021 (patch) | |
| tree | 6698ac68f45940456cafb56aaaf0dec36bfb408f /pretyping/cases.ml | |
| parent | f6382ef326099651cd051aa907b4e9ac6c905698 (diff) | |
Change interface of refresh universes to get a pbty argument instead of
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 50396d854..3f1bead36 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = map_constr_with_full_binders push_binder aux x t | Evar ev -> let ty = get_type_of env sigma t in - let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let inst = List.map_i (fun i _ -> @@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of env !evdref t in - Evarutil.evd_comb1 (refresh_universes false env) evdref ty + Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in let depvl = free_rels ty in |