diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 0f9331ff5..9eac4fbae 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -523,6 +523,9 @@ module Coercion = struct | Some (init, cur) -> (isevars, cj) + let inh_conv_coerce_rigid_to _ _ _ _ _ = + failwith "inh_conv_coerce_rigid_to: TODO" + let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = (* (try *) (* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *) |