Simplified the way internalization_data (i.e. bindings of bound vars

to their signature of implicit positions and scopes) is computed.
A bit of documentation in constrintern.mli.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 28 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1dd221f69..e1f1c50b4 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -26,44 +26,43 @@ open Pretyping
       - check all variables are bound
       - make absolute the references to global objets
    - resolution of symbolic notations using scopes
-   - insert existential variables for implicit arguments
+   - insertion of implicit arguments
 
-   To interpret implicits and arg scopes of recursive variables while
-   internalizing inductive types and recursive definitions, and also
+   To interpret implicit arguments and arg scopes of recursive variables
+   while internalizing inductive types and recursive definitions, and also
    projection while typing records.
 
    the third and fourth arguments associate a list of implicit
    positions and scopes to identifiers declared in the [rel_context]
    of [env] *)
 
-type var_internalization_type = Inductive | Recursive | Method
+type var_internalization_type =
+  | Inductive of identifier list (* list of params *)
+  | Recursive
+  | Method
 
 type var_internalization_data =
     var_internalization_type *
+      (** type of the "free" variable, for coqdoc, e.g. while typing the
+	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
     identifier list *
-    Impargs.implicits_list *
-    scope_name option list
+      (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+          in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+    Impargs.implicits_list * (** signature of impargs of the variable *)
+    scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env =
     (identifier * var_internalization_data) list
 
-(** Contains also a list of identifiers to automatically apply to the variables*)
-type full_internalization_env =
-    identifier list * internalization_env
-
-val empty_internalization_env : full_internalization_env
+val empty_internalization_env : internalization_env
 
 val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
-val set_internalization_env_params :
-  internalization_env -> identifier list -> full_internalization_env
-
-val compute_full_internalization_env : env ->
-  var_internalization_type ->
-  identifier list -> identifier list -> types list ->
-  Impargs.manual_explicitation list list -> full_internalization_env
+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
 
@@ -78,7 +77,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 val intern_type : evar_map -> env -> constr_expr -> rawconstr
 
 val intern_gen : bool -> evar_map -> env ->
-  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
 val intern_pattern : env -> cases_pattern_expr ->
@@ -92,7 +91,7 @@ val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder
 (** Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
 (** Particular instances *)
@@ -100,33 +99,33 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env ->
   constr_expr -> constr
 
-val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
+val interp_type : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
 val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types -> constr
 
 (** 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:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
+  ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
 
 val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_internalization_env ->
+  env -> ?impls:internalization_env ->
   constr_expr -> types * manual_implicits
 
 val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_internalization_env ->
+  env -> ?impls:internalization_env ->
   constr_expr -> constr * manual_implicits
 
 val interp_casted_constr_evars : evar_map ref -> env ->
-  ?impls:full_internalization_env -> constr_expr -> types -> constr
+  ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env ->
+val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
 (** {6 Build a judgment  } *)
@@ -174,7 +173,7 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (** Interprets into a abbreviatable constr *)
 
-val interp_aconstr : ?impls:full_internalization_env ->
+val interp_aconstr : ?impls:internalization_env ->
   identifier list * identifier list -> constr_expr -> interpretation
 
 (** Globalization leak for Grammar *)