From a1e5a87c9d4368fe17d93988b010acfb1c96771b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 17:03:10 +0100
Subject: Cleaning phase around local binder at glob level:

Aligned the type binder_data to the naming scheme used in (raw)
local_binder and Rel.Declaration.t. Made some code factorization.

Still to do: align type Glob_term.glob_binder to the Assum/Def format
too.

Note: this includes fix of anomaly with 'pat in cofix (dec77f282).
---
 interp/constrintern.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 61e7c6f5cb..021b565c8f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -75,8 +75,6 @@ type ltac_sign = {
 
 val empty_ltac_sign : ltac_sign
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
-
 (** {6 Internalization performs interpretation of global names and notations } *)
 
 val intern_constr : env -> constr_expr -> glob_constr
-- 
cgit v1.2.3


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/constrintern.mli')

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


From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 interp/constrintern.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d99747be56..e45de25887 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_decl list
+val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -157,16 +157,16 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-  env -> evar_map ref -> local_binder list ->
+  env -> evar_map ref -> local_binder_expr list ->
   internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
 (*   ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
+(*   env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
   
 (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list ->  *)
+(*   env -> evar_map -> local_binder_expr list ->  *)
 (*   internalization_env *  *)
 (*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
 
-- 
cgit v1.2.3