diff options
Diffstat (limited to 'plugins/subtac/subtac_coercion.ml')
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 4dd3dd32be..8cf28a0dd6 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -166,7 +166,7 @@ module Coercion = struct | Type x, Type y when x = y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> - let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in + let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) |