From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
---
 pretyping/typeclasses.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e95aba695d..0c30296d35 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -67,7 +67,7 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses *
 val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
 
 (** Just return None if not a class *)
-val class_of_constr : evar_map -> EConstr.constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
+val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option
   
 val instance_impl : instance -> global_reference
 
-- 
cgit v1.2.3