aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-03-24 18:19:08 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-03-24 18:22:26 +0100
commita6d6bca5f024cbdc35924c2cb5e399eb8a2d9c16 (patch)
tree972d67263b86466b67ad3ed744042cf6aff31f12
parent866b7539cca2bd48c230bc6ddf3acea89cb1450a (diff)
Fix handling of arity of definitional classes.
The user-provided sort was ignored for them.
-rw-r--r--theories/Classes/CMorphisms.v2
-rw-r--r--toplevel/record.ml8
2 files changed, 5 insertions, 5 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c41eb2fa2..10f18fe70 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive
Section Normalize.
Context (A : Type).
- Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+ Class Normalizes (m : crelation A) (m' : crelation A) :=
normalizes : relation_equivalence m m'.
(** Current strategy: add [flip] everywhere and reduce using [subrelation]
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c5ae7e891..6bdcdef01 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,8 +135,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let _, univ = compute_constructor_level evars env_ar newfs in
let ctx, aritysort = Reduction.dest_arity env0 arity in
assert(List.is_empty ctx); (* Ensured by above analysis *)
- if Sorts.is_prop aritysort ||
- (Sorts.is_set aritysort && is_impredicative_set env0) then
+ if not def && (Sorts.is_prop aritysort ||
+ (Sorts.is_set aritysort && is_impredicative_set env0)) then
arity, evars
else
let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
@@ -408,9 +408,9 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
match fields with
| [(Name proj_name, _, field)] when def ->
let class_body = it_mkLambda_or_LetIn field params in
- let _class_type = it_mkProd_or_LetIn arity params in
+ let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
- Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
+ Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in