From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- pretyping/arguments_renaming.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/arguments_renaming.ml') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ea33f1c0d..d59102b6c 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -10,6 +10,7 @@ open Names open Globnames open Term +open Constr open Environ open Util open Libobject @@ -103,7 +104,7 @@ let rename_type_of_constructor env cstruct = let rename_typing env c = let j = Typeops.infer env c in let j' = - match kind_of_term c with + match kind c with | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) } | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) } | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) } -- cgit v1.2.3