From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Nov 2017 18:14:38 +0100
Subject: [api] Deprecate all legacy uses of Name.Id in core.

This is a first step towards some of the solutions proposed in #6008.
---
 kernel/type_errors.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index bbaf569d39..9813fc566e 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -44,7 +44,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of identifier * 'constr
+  | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
-- 
cgit v1.2.3