diff options
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 ae0b885e47..db82c205cb 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -119,13 +119,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 (LocalAssum (Name id,fullarity)) env0) in |