From 30a2f4c5469e25038f5720f03e948519efeef48d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Feb 2020 13:54:23 +0100
Subject: ReferenceVariables error contains a globref instead of a constr

The previous system was from before globref was in the kernel.
---
 kernel/type_errors.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0f29717f12..d9842ecefa 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of Id.t * 'constr
+  | ReferenceVariables of Id.t * GlobRef.t
   | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
       * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -102,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
 
-val error_reference_variables : env -> Id.t -> constr -> 'a
+val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
 
 val error_elim_arity :
   env -> pinductive -> constr -> unsafe_judgment ->
-- 
cgit v1.2.3