diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ae1c4eea0..54621eb9d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -399,7 +399,7 @@ type coercion = { coercion_params : int; } -(* Calcul de l'arit้ d'une classe *) +(* Computation of the class arity *) let reference_arity_length ref = let t = Universes.unsafe_type_of_global ref in |