diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8d87f6e99c..1cc072a2a2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -89,7 +89,7 @@ sig type t val compare : t -> t -> int val equal : t -> t -> bool - val print : t -> std_ppcmds + val print : t -> Pp.t end type 'a t val empty : 'a t @@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* rajouter une coercion dans le graphe *) let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds) + : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) let install_path_printer f = path_printer := f @@ -403,7 +403,7 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t = Universes.unsafe_type_of_global ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = |