diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 13 |
2 files changed, 10 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ffa2484eef..2875511d35 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1087,7 +1087,7 @@ let interp_recursive isfix fixl notations = | Some ls , Some us -> if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then error "(co)-recursive definitions should all have the same universe binders"; - Some (ls @ us)) fixl None in + Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in let fixctxs, fiximppairs, fixannots = diff --git a/toplevel/record.ml b/toplevel/record.ml index 3151b13726..e9de6b5324 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 |