From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e248436ec..c0f564dc3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -787,7 +787,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = - let mp, dp, l = repr_mind kn in + let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) -- cgit v1.2.3