diff options
| author | Matthieu Sozeau | 2016-03-17 20:23:00 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-03-17 20:24:46 +0100 |
| commit | c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f (patch) | |
| tree | 13c0f493133186efce01afee6715297e3479298f /toplevel | |
| parent | bcee0b4d6ca113d225fa7df1cbcfa33812b0bd46 (diff) | |
Fix bug #4627: records with no declared arity can be template polymorphic.
As if we were adding : Type. Consistent with inductives with no
declared arity.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 200d1a9387..c5ae7e8913 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -114,13 +114,13 @@ let typecheck_params_and_fields def id pl t ps nots fs = (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 (* (not def) *) l; + | Some l -> evars := Evd.make_flexible_variable !evars true l; sred, true | None -> s, false) | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) | None -> - let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in - mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false + let uvarkind = Evd.univ_flexible_alg in + mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true in let fullarity = it_mkProd_or_LetIn t' newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in |