diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-30 23:52:58 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-29 11:52:52 +0200 |
| commit | c200c2b41e88dd7d4a1b9e90e0c35a7ed047309c (patch) | |
| tree | 1ff729200d9e587ace74d4b83611af4a69e6afdf /toplevel | |
| parent | d4cdb7e41844e1bb77bac9a7b9df423364b996e2 (diff) | |
Univs: Fix bug #4726
When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 3151b1372..e9de6b532 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -114,14 +114,19 @@ let typecheck_params_and_fields def id pl t ps nots fs = let t', template = match t with | Some t -> let env = push_rel_context newps env0 in + let poly = + match t with + | CSort (_, Misctypes.GType []) -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in let sred = Reductionops.whd_betadeltaiota env !evars s in (match kind_of_term sred with | Sort s' -> - (match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true l; - sred, true - | None -> s, false) + (if poly then + match Evd.is_sort_variable !evars s' with + | Some l -> evars := Evd.make_flexible_variable !evars true l; + sred, true + | None -> s, false + else s, false) | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in |