From 659795aeb2cd329eab5c4a92adbde724573dd106 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 10 Feb 2011 14:10:51 +0000
Subject: More comments and less doublons in some mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13820 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml          |  2 --
 interp/constrintern.mli         | 14 ++++++--------
 interp/implicit_quantifiers.mli |  2 +-
 3 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8454b8fef..6072549c2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1451,8 +1451,6 @@ let intern_pattern env patt =
 	user_err_loc (loc,"internalize",explain_internalization_error e)
 
 
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 59afcd313..12dc6be16 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -64,8 +64,6 @@ val compute_internalization_env : env -> var_internalization_type ->
   identifier list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
@@ -112,15 +110,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
 (** Accepting evars and giving back the manual implicits in addition. *)
 
 val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
-  ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
+  ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
 
 val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
   env -> ?impls:internalization_env ->
-  constr_expr -> types * manual_implicits
+  constr_expr -> types * Impargs.manual_implicits
 
 val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
   env -> ?impls:internalization_env ->
-  constr_expr -> constr * manual_implicits
+  constr_expr -> constr * Impargs.manual_implicits
 
 val interp_casted_constr_evars : evar_map ref -> env ->
   ?impls:internalization_env -> constr_expr -> types -> constr
@@ -155,13 +153,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
 val interp_context_gen : (env -> glob_constr -> types) ->
   (env -> glob_constr -> unsafe_judgment) ->
   ?global_level:bool ->
-  evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+  evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
   
 val interp_context : ?global_level:bool ->
-  evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+  evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
 
 val interp_context_evars : ?global_level:bool ->
-  evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
+  evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits
 
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 05f54ec75..ce518a9cb 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-- 
cgit v1.2.3