diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /kernel/mod_typing.ml | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f68dd158c2..421d932d9a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -76,7 +76,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = as long as they have the right type *) let c', univs, ctx' = match cb.const_universes, ctx with - | Monomorphic_const _, None -> + | Monomorphic _, None -> let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in @@ -90,8 +90,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Primitive _ -> error_incorrect_with_constraint lab in - c', Monomorphic_const Univ.ContextSet.empty, cst - | Polymorphic_const uctx, Some ctx -> + c', Monomorphic Univ.ContextSet.empty, cst + | Polymorphic uctx, Some ctx -> let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab @@ -114,7 +114,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = in if not (Univ.Constraint.is_empty cst) then error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.Constraint.empty + c, Polymorphic ctx, Univ.Constraint.empty | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in |