Add the source and target classes to the coercion table

`coe_source` and `coe_target` fields of type `cl_typ` have been added to
`coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a
coercion. The `coercion` record has also been replaced with `coe_info_typ`.

1 files changed, 13 insertions, 13 deletions

diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 15d8ebc4b5..86b15739f9 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -237,24 +237,24 @@ let open_coercion i o =
     cache_coercion o
 
 let discharge_coercion (_, c) =
-  if c.coercion_local then None
+  if c.coe_local then None
   else
     let n =
       try
-        let ins = Lib.section_instance c.coercion_type in
+        let ins = Lib.section_instance c.coe_value in
         Array.length (snd ins)
       with Not_found -> 0
     in
     let nc = { c with
-      coercion_params = n + c.coercion_params;
-      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
+      coe_param = n + c.coe_param;
+      coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection;
     } in
     Some nc
 
 let classify_coercion obj =
-  if obj.coercion_local then Dispose else Substitute obj
+  if obj.coe_local then Dispose else Substitute obj
 
-let inCoercion : coercion -> obj =
+let inCoercion : coe_info_typ -> obj =
   declare_object {(default_object "COERCION") with
     open_function = simple_open open_coercion;
     cache_function = cache_coercion;
@@ -269,13 +269,13 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
     | _ -> None
   in
   let c = {
-    coercion_type = coef;
-    coercion_local = local;
-    coercion_is_id = isid;
-    coercion_is_proj = isproj;
-    coercion_source = cls;
-    coercion_target = clt;
-    coercion_params = ps;
+    coe_value = coef;
+    coe_local = local;
+    coe_is_identity = isid;
+    coe_is_projection = isproj;
+    coe_source = cls;
+    coe_target = clt;
+    coe_param = ps;
   } in
   Lib.add_anonymous_leaf (inCoercion c)