diff options
| author | Gaëtan Gilbert | 2020-07-09 15:55:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-21 15:26:01 +0200 |
| commit | 7461fe4f55ad9ee7c55c9b060e74a49d173b4ce7 (patch) | |
| tree | 150713e14e25ff3358a7bd18a49b277d6fcedff4 /kernel/term_typing.ml | |
| parent | f44202e28f38aa900801b0c90514690b6a401bed (diff) | |
Turn various anomalies into regular errors in primitive declaration path
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 04e7a81697..48567aa564 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = univs, typ | Some (typ,Monomorphic_entry uctx) -> - assert (AUContext.is_empty auctx); + assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *) let env = push_context_set ~strict:true uctx env in let u = Instance.empty in let typ = @@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = Monomorphic uctx, typ | Some (typ,Polymorphic_entry (unames,uctx)) -> - assert (not (AUContext.is_empty auctx)); - (* push_context will check that the universes aren't repeated in the instance - so comparing the sizes works *) - assert (AUContext.size auctx = UContext.size uctx); - (* No polymorphic primitive uses constraints currently *) - assert (Constraint.is_empty (UContext.constraints uctx)); + assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *) + (* [push_context] will check that the universes aren't repeated in + the instance so comparing the sizes works. No polymorphic + primitive uses constraints currently. *) + if not (AUContext.size auctx = UContext.size uctx + && Constraint.is_empty (UContext.constraints uctx)) + then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++ + str (op_or_type_to_string p)); let env = push_context ~strict:false uctx env in (* Now we know that uctx matches the auctx *) let typ = (Typeops.infer_type env typ).utj_val in |