diff options
| author | Pierre-Marie Pédrot | 2016-03-20 16:37:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 16:37:09 +0100 |
| commit | 2349d740caa4d9248ba5485aebbcce9ec18d3fd2 (patch) | |
| tree | 18a3bc56f498049b28bc0d7a3266c8e6f5dbc272 /toplevel | |
| parent | 1890a2cdc0dcda7335d7f81fc9ce77c0debc4324 (diff) | |
| parent | 09c2011fbdbb2ac1ce33e5abe52d93b907b21a3c (diff) | |
Merge branch 'v8.5'
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 |