diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 539e186d53..30fd8281e1 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -465,7 +465,7 @@ module Coercion = struct (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) = + let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) = (* (try *) (* trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *) (* Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *) |