From 68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:00:07 +0100
Subject: Merging glob_binder and glob_decl.

---
 interp/constrintern.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 021b565c8f..d99747be56 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,7 +88,7 @@ val intern_gen : typing_constraint -> env ->
 val intern_pattern : env -> cases_pattern_expr ->
   Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
+val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
-- 
cgit v1.2.3