Adapt coercion code to work with projections as target classes.

5 files changed, 32 insertions, 15 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 86b789f7d3..9041a0af46 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -31,6 +31,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of constant
   | CL_IND of inductive
+  | CL_PROJ of projection
 
 type cl_info_typ = {
   cl_param : int
@@ -194,6 +195,7 @@ let find_class_type sigma t =
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, Univ.Instance.empty, args
     | Const (sp,u) -> CL_CONST sp, u, args
+    | Proj (p, c) -> CL_PROJ p, Univ.Instance.empty, c :: args
     | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
     | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
     | Sort _ -> CL_SORT, Univ.Instance.empty, []
@@ -204,6 +206,9 @@ let subst_cl_typ subst ct = match ct with
     CL_SORT
   | CL_FUN
   | CL_SECVAR _ -> ct
+  | CL_PROJ c ->
+    let c',t = subst_con_kn subst c in
+      if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
       let c',t = subst_con_kn subst c in
 	if c' == c then ct else
@@ -239,7 +244,7 @@ let class_args_of env sigma c = pi3 (find_class_type sigma c)
 let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp ->
+  | CL_CONST sp | CL_PROJ sp ->
       string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_IND sp ->
       string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
@@ -395,12 +400,18 @@ type coercion = {
 (* Calcul de l'arit้ d'une classe *)
 
 let reference_arity_length ref =
-  let t,_ = Universes.type_of_global ref in
+  let t = Universes.unsafe_type_of_global ref in
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))
 
+let projection_arity_length p =
+  let len = reference_arity_length (ConstRef p) in
+  let pb = Environ.lookup_projection p (Global.env ()) in 
+    len - pb.Declarations.proj_npars
+
 let class_params = function
   | CL_FUN | CL_SORT -> 0
   | CL_CONST sp -> reference_arity_length (ConstRef sp)
+  | CL_PROJ sp -> projection_arity_length sp
   | CL_SECVAR sp -> reference_arity_length (VarRef sp)
   | CL_IND sp  -> reference_arity_length (IndRef sp)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 3251dc4eb9..e39b2bba42 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -19,6 +19,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of constant
   | CL_IND of inductive
+  | CL_PROJ of projection
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
diff --git a/test-suite/bugs/closed/HoTT_coq_081.v b/test-suite/bugs/closed/HoTT_coq_081.v
new file mode 100644
index 0000000000..ac27dea71f
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_081.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category (A : Type) :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+
+Record foo { A: Type } := { C : category A; x : ob C; y :> hom _ x x }.
+Definition comp A (C : category A) (x : C) (f : hom _ x x) := f.
+
+Definition bar A (f : @foo A) := @comp _ _ _ f.
+
+(* Toplevel input, characters 0-42:
+Error: Cannot find the target class. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_081.v b/test-suite/bugs/opened/HoTT_coq_081.v
deleted file mode 100644
index bcd12aa691..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_081.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category :=
-  { ob :> Type;
-    hom : ob -> ob -> Type
-  }.
-
-Fail Record foo := { C : category; x :> ob C }.
-(* Toplevel input, characters 0-42:
-Error: Cannot find the target class. *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 635b1c52c0..a6591f0d3b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -72,6 +72,7 @@ let check_reference_arity ref =
 let check_arity = function
   | CL_FUN | CL_SORT -> ()
   | CL_CONST cst -> check_reference_arity (ConstRef cst)
+  | CL_PROJ cst -> check_reference_arity (ConstRef cst)
   | CL_SECVAR id -> check_reference_arity (VarRef id)
   | CL_IND kn -> check_reference_arity (IndRef kn)
 
@@ -167,7 +168,7 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp -> Label.to_string (con_label sp)
+  | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
   | CL_IND (sp,_) -> Label.to_string (mind_label sp)
   | CL_SECVAR id -> Id.to_string id