From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/class.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'vernac/class.ml')

diff --git a/vernac/class.ml b/vernac/class.ml
index 59d93310..614b2181 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -37,7 +37,7 @@ type coercion_error_kind =
   | ForbiddenSourceClass of cl_typ
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
-  | NotAClass of global_reference
+  | NotAClass of GlobRef.t
 
 exception CoercionError of coercion_error_kind
 
@@ -67,13 +67,13 @@ let explain_coercion_error g = function
 let check_reference_arity ref =
   let env = Global.env () in
   let c, _ = Global.type_of_global_in_context env ref in
-  if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
+  if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass 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_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
   | CL_SECVAR id -> check_reference_arity (VarRef id)
   | CL_IND kn -> check_reference_arity (IndRef kn)
 
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
 
 let class_of_global = function
   | ConstRef sp -> 
-    if Environ.is_projection sp (Global.env ()) 
-    then CL_PROJ sp else CL_CONST sp
+    (match Recordops.find_primitive_projection sp with
+     | Some p -> CL_PROJ p | None -> CL_CONST sp)
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
     CL_FUN
   else
     match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
-    | CL_CONST p when Environ.is_projection p (Global.env ()) -> 
-      CL_PROJ p
+    | CL_CONST p when Recordops.is_primitive_projection p ->
+      CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
     | x -> x
       
 let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+  | CL_CONST sp -> Label.to_string (Constant.label sp)
+  | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
   | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
   | CL_SECVAR id -> Id.to_string id
 
@@ -181,6 +182,7 @@ let build_id_coercion idf_opt source poly =
   let sigma, vs = match source with
     | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp)
     | _ -> error_not_transparent source in
+  let vs = EConstr.Unsafe.to_constr vs in
   let c = match constant_opt_value_in env (destConst vs) with
     | Some c -> c
     | None -> error_not_transparent source in
@@ -302,12 +304,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly local ref =
-  let stre = match local with
+  let local = match local with
+  | Discharge
   | Local -> true
   | Global -> false
-  | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref ~local:stre poly in
+  let () = try_add_new_coercion ref ~local poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-- 
cgit v1.2.3